Next Prev Up
LeftChopImpMoreRule

⊢ f ⊃ more ⇒ ⊢ f ; g ⊃ more LeftChopImpMoreRule

Proof:

1
⊢ f ⊃more
given
2
⊢ f ; g ⊃more ; g
1,LeftChopImpChop
3
⊢ more ; g ⊃more
MoreChopImpMore
4
⊢ f ; g ⊃more
2, 3,ImpChain

qed

Next Prev Up

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