Next Prev Up
BaChopImpChopBa

⊢ f ⊃ g ; g1 ⊃ g ; ( f ∧ g1) BaChopImpChopBa

Proof:

1
⊢ f ⊃ (g1 ⊃ f ∧ g1)
PTL
2
⊢ (g1 ⊃ f ∧ g1) ⊃ g ; g1 ⊃ g ; ( f ∧ g1)
BaRightChopImpChop
3
⊢ f ⊃ g ; g1 ⊃ g ; ( f ∧ g1)
1, 2,Prop

qed

Next Prev Up

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