Theorem oran2 84

Description: Disjunction expressed with conjunction.

Assertion

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

Proof of Theorem oran2

Step	Hyp	Ref	Expression
1		anor1 80	. . 3 (a ^ b_|_) = (a_|_ v b)_|_
2	1	ax-r1 34	. 2 (a_|_ v b)_|_ = (a ^ b_|_)
3	2	con3 65	1 (a_|_ v b) = (a ^ b_|_)_|_

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

This theorem is referenced by:  wql2lem3 282  wdf-c2 366  u1lemnanb 637  u2lemnanb 638  u3lemnanb 639  u4lemnanb 640  u5lemnanb 641  u3lemnona 649  u4lemnob 655  u4lem5 746  u4lem5n 748  u2lem7n 757  bi4 822  negantlem8 838  neg3antlem2 847  mhlem2 860  marsdenlem3 864  marsdenlem4 865  oa4cl 1007

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

metamath.org