Next Prev Up
ChopMoreImpMore

⊢ f ; more ⊃more ChopMoreImpMore

Proof:

1
⊢ f ; more ⊃more
ChopImpDiamond
2
⊢ more ⊃more
PTL
3
⊢ f ; more ⊃more
1, 2,ImpChain

qed

Next Prev Up

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