Prev Up
BfAndChopImport

⊢ f ∧ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g BfAndChopImport

Proof:

1
f ⊃ (f1 ⊃ f ∧ f1)
Prop
2
f ⊃ (f1 ⊃ f ∧ f1)
1,BfImpBfRule
3
(f1 ⊃ f ∧ f1) ⊃ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g
BfChopImpChop
4
f ∧ (f1 ⌢ g) ⊃ (f ∧ f1) ⌢ g
2, 3,Prop

qed

Prev Up

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