Next Prev Up
BoxAndChopImport

⊢ h ∧ f ; g ⊃ f ; (h ∧ g) BoxAndChopImport

Proof:

1
⊢ h ⊃ g ⊃ (h ∧ g)
Prop
2
⊢ h ⊃ (g ⊃ (h ∧ g))
1,BoxImpBoxRule
3
⊢ (g ⊃ (h ∧ g)) ⊃ f ; g ⊃ f ; (h ∧ g)
BoxChopImpChop
4
⊢ h ∧ f ; g ⊃ f ; (h ∧ g)
2, 3,Prop

qed

Next Prev Up

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