Next Prev Up
BiChopImpChop

⊢ (f ⊃ f1) ⊃ (f ; g) ⊃ (f1 ; g) BiChopImpChop

Proof:

1
⊢ g ⊃ g
Prop
2
⊢ (g ⊃ g)
1,BoxGen
3
⊢ (f ⊃ f1) ∧ (g ⊃ g) ⊃ (f ; g) ⊃ (f1 ; g)
BiBoxChopImpChop
4
⊢ (f ⊃ f1) ⊃ (f ; g) ⊃ (f1 ; g)
2, 3,Prop

qed

Next Prev Up

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