Next Prev Up
AndChopB

⊢ (f ∧ f1) ; g ⊃ f1 ; g AndChopB

Proof:

1
⊢ f ∧ f1 ⊃ f1
PTL
2
⊢ (f ∧ f1 ⊃ f1)
1,BiGen
3
⊢ (f ∧ f1 ⊃ f1) ⊃ (f ∧ f1) ; g ⊃ f1 ; g
2,BiChopImpChop
4
⊢ (f ∧ f1) ; g ⊃ f1 ; g
2, 3,MP

qed

Next Prev Up

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