Next Up
BfChopImpChop

⊢ (f ⊃ f1) ⊃ (f ⌢ g) ⊃ (f1 ⌢ g) BfChopImpChop

Proof:

1
g ⊃ g
Prop
2
(g ⊃ g)
1,BoxGen
3
(f ⊃ f1) ∧ (g ⊃ g) ⊃ (f ⌢ g) ⊃ (f1 ⌢ g)
BfAndBoxImpChopImpChop
4
(f ⊃ f1) ⊃ (f ⌢ g) ⊃ (f1 ⌢ g)
2, 3,Prop

qed

Next Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023