BfAndEqv

(f g) f g BfAndEqv

Proof:

1
(f g) f
2
(f g) f
3
(f g) g
4
(f g) g
5
f (g (f g))
6
f (g (f g))
7
(g (f g)) ( g (f g))
8
f g (f g)
6, 7,Prop
9
(f g) f g
2, 4, 8,Prop

qed

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