Next Prev Up
AndChopCommute

⊢ (f ∧ f1) ; g ≡ (f1 ∧ f) ; g AndChopCommute

Proof:

1
⊢ f ∧ f1 ≡ f1 ∧ f
Prop
2
⊢ (f ∧ f1) ; g ≡ (f1 ∧ f) ; g
1,LeftChopEqvChop

qed

Next Prev Up

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