Next Prev Up
MultChopImpCS

⊢ f1 ⊃ g, …, ⊢ fn ⊃ g ⇒ ⊢ (f1 ; … ; fn) ⊃ g∗ MultChopImpCS

Proof:

1
⊢ fi ⊃ g, for 1 ≤ i ≤ n
given
2
⊢ f1 ; … ; fn ⊃ g ; … ; g
1,MultChopImpChop
3
⊢ g ; … ; g ⊃ g∗
ChopGroupImpCS
4
⊢ f1 ; … ; fn ⊃ g∗
2, 3,ImpChain

qed

Next Prev Up

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