Next Prev Up
StateAndChopImpChopRule

⊢ w ∧ f ⊃ f1 ⇒ ⊢ w ∧ (f ; g) ⊃ (f1 ; g) StateAndChopImpChopRule

Proof:

1
⊢ w ∧ f ⊃ f1
given
2
⊢ (w ∧ f) ; g ⊃ f1 ; g
1,LeftChopImpChop
3
⊢ (w ∧ f) ; g ≡ w ∧ (f ; g)
StateAndChop
4
⊢ w ∧ f ; g ⊃ f1 ; g
2, 3,Prop

qed

Next Prev Up

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