Next Prev Up
RightChopImpMoreRule

⊢ g ⊃ more ⇒ ⊢ f ; g ⊃ more RightChopImpMoreRule

Proof:

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

qed

Next Prev Up

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