Prev Up
ChopAndNotChopImp

⊢ f ⌢ g ∧¬(f ⌢ g1) ⊃ f ⌢ (g ∧¬g1) ChopAndNotChopImp

Proof:

1
g ⊃ (g ∧¬g1) ∨ g1
Prop
2
f ⌢ g ⊃ f ⌢ (g ∧¬g1) ∨ f ⌢ g1
1,LeftChopImpChop
3
f ⌢ g ∧¬(f ⌢ g1) ⊃ f ⌢ (g ∧¬g1)
2,Prop

qed

Prev Up

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