Next Prev Up
ChopAndYieldsMP

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

Proof:

1
⊢ f ; g ∧ f (g ⊃ g1) ⊃ f ; (g ∧ (g ⊃ g1))
ChopAndYieldsImp
2
⊢ g ∧ (g ⊃ g1) ⊃ g1
Prop
3
⊢ f ; (g ∧ (g ⊃ g1)) ⊃ f ; g1
2,RightChopImpChop
4
⊢ f ; g ∧ f (g ⊃ g1) ⊃ f ; g1
1, 3,ImpChain

qed

Next Prev Up

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