Theorem di 118

Description: Dishkant implication.

Assertion

Ref	Expression
di	((a ^ b) == a) = (a_|_ v (a ^ b))

Proof of Theorem di

Step	Hyp	Ref	Expression
1		conb 114	. . 3 ((b_|_ v a_|_)_|_ == a) = ((b_|_ v a_|_)_|__|_ == a_|_)
2		ax-a1 29	. . . . . 6 (b_|_ v a_|_) = (b_|_ v a_|_)_|__|_
3	2	ax-r1 34	. . . . 5 (b_|_ v a_|_)_|__|_ = (b_|_ v a_|_)
4	3	rbi 90	. . . 4 ((b_|_ v a_|_)_|__|_ == a_|_) = ((b_|_ v a_|_) == a_|_)
5		mi 117	. . . 4 ((b_|_ v a_|_) == a_|_) = (a_|_ v (b_|__|_ ^ a_|__|_))
6	4, 5	ax-r2 35	. . 3 ((b_|_ v a_|_)_|__|_ == a_|_) = (a_|_ v (b_|__|_ ^ a_|__|_))
7	1, 6	ax-r2 35	. 2 ((b_|_ v a_|_)_|_ == a) = (a_|_ v (b_|__|_ ^ a_|__|_))
8		ancom 68	. . . 4 (a ^ b) = (b ^ a)
9		df-a 39	. . . 4 (b ^ a) = (b_|_ v a_|_)_|_
10	8, 9	ax-r2 35	. . 3 (a ^ b) = (b_|_ v a_|_)_|_
11	10	rbi 90	. 2 ((a ^ b) == a) = ((b_|_ v a_|_)_|_ == a)
12		ax-a1 29	. . . . 5 b = b_|__|_
13		ax-a1 29	. . . . 5 a = a_|__|_
14	12, 13	2an 72	. . . 4 (b ^ a) = (b_|__|_ ^ a_|__|_)
15	8, 14	ax-r2 35	. . 3 (a ^ b) = (b_|__|_ ^ a_|__|_)
16	15	lor 66	. 2 (a_|_ v (a ^ b)) = (a_|_ v (b_|__|_ ^ a_|__|_))
17	7, 11, 16	3tr1 60	1 ((a ^ b) == a) = (a_|_ v (a ^ b))

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41

metamath.org