Next Prev Up
ChopAndBaImport

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

Proof:

1
⊢ g ∧ (f ; f1) ⊃ (g ∧ f) ; (g ∧ f1)
BaAndChopImport
2
⊢ (g ∧ f) ; (g ∧ f1) ≡ (f ∧ g) ; (f1 ∧ g)
AndChopAndCommute
2
⊢ (f ; f1) ∧ g ⊃ (f ∧ g) ; (f1 ∧ g)
1, 2,Prop

qed

Next Prev Up

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