Next Prev Up
BfMoreImpImpBfSkipImp

⊢ (more ⊃ f) ⊃ (skip ⊃ f) BfMoreImpImpBfSkipImp

Proof:

1
more ⊃ skip
VPTL
2
(more ⊃ f) ⊃ (skip ⊃ f)
1,Prop
3
(more ⊃ f) ⊃ (skip ⊃ f)
2,BfImpBfRule

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024