Theorem ni31 242

Description: Equivalence for Kalmbach implication.

Assertion

Ref	Expression
ni31	(a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))

Proof of Theorem ni31

Step	Hyp	Ref	Expression
1		df-i3 45	. . 3 (a ->3 b) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))
2		oran 79	. . . 4 (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))) = (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ (a ^ (a_|_ v b))_|_)_|_
3		oran 79	. . . . . . . 8 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((a_|_ ^ b)_|_ ^ (a_|_ ^ b_|_)_|_)_|_
4		anor2 81	. . . . . . . . . . 11 (a_|_ ^ b) = (a v b_|_)_|_
5	4	con2 64	. . . . . . . . . 10 (a_|_ ^ b)_|_ = (a v b_|_)
6		oran 79	. . . . . . . . . . 11 (a v b) = (a_|_ ^ b_|_)_|_
7	6	ax-r1 34	. . . . . . . . . 10 (a_|_ ^ b_|_)_|_ = (a v b)
8	5, 7	2an 72	. . . . . . . . 9 ((a_|_ ^ b)_|_ ^ (a_|_ ^ b_|_)_|_) = ((a v b_|_) ^ (a v b))
9	8	ax-r4 36	. . . . . . . 8 ((a_|_ ^ b)_|_ ^ (a_|_ ^ b_|_)_|_)_|_ = ((a v b_|_) ^ (a v b))_|_
10	3, 9	ax-r2 35	. . . . . . 7 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((a v b_|_) ^ (a v b))_|_
11	10	con2 64	. . . . . 6 ((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ = ((a v b_|_) ^ (a v b))
12		df-a 39	. . . . . . . 8 (a ^ (a_|_ v b)) = (a_|_ v (a_|_ v b)_|_)_|_
13		anor1 80	. . . . . . . . . . 11 (a ^ b_|_) = (a_|_ v b)_|_
14	13	ax-r1 34	. . . . . . . . . 10 (a_|_ v b)_|_ = (a ^ b_|_)
15	14	lor 66	. . . . . . . . 9 (a_|_ v (a_|_ v b)_|_) = (a_|_ v (a ^ b_|_))
16	15	ax-r4 36	. . . . . . . 8 (a_|_ v (a_|_ v b)_|_)_|_ = (a_|_ v (a ^ b_|_))_|_
17	12, 16	ax-r2 35	. . . . . . 7 (a ^ (a_|_ v b)) = (a_|_ v (a ^ b_|_))_|_
18	17	con2 64	. . . . . 6 (a ^ (a_|_ v b))_|_ = (a_|_ v (a ^ b_|_))
19	11, 18	2an 72	. . . . 5 (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ (a ^ (a_|_ v b))_|_) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))
20	19	ax-r4 36	. . . 4 (((a_|_ ^ b) v (a_|_ ^ b_|_))_|_ ^ (a ^ (a_|_ v b))_|_)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))_|_
21	2, 20	ax-r2 35	. . 3 (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))_|_
22	1, 21	ax-r2 35	. 2 (a ->3 b) = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))_|_
23	22	con2 64	1 (a ->3 b)_|_ = (((a v b_|_) ^ (a v b)) ^ (a_|_ v (a ^ b_|_)))

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7   ->3 wi3 15

This theorem is referenced by:  ud3lem0c 271

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

This theorem depends on definitions:  df-a 39  df-i3 45

metamath.org