Next Prev Up
BaAndChopImport

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

Proof:

1
⊢ f ⊃ f
BaImpBi
2
⊢ f ∧ (g ; g1) ⊃ (f ∧ g) ; g1
BiAndChopImport
3
⊢ f ⊃ f
BaImpBt
4
⊢ f ∧ (f ∧ g) ; g1 ⊃ (f ∧ g) ; (f ∧ g1)
BoxAndChopImport
5
⊢ f ∧ (g ; g1) ⊃ (f ∧ g) ; (f ∧ g1)
1, 2, 3, 4,Prop

qed

Next Prev Up

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