Theorem oran1 83

Description: Disjunction expressed with conjunction.

Assertion

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

Proof of Theorem oran1

Step	Hyp	Ref	Expression
1		anor2 81	. . 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:  u3lemnana 629  u5lemnana 631  u1lemnab 632  u2lemnab 633  u3lemnab 634  u4lemnab 635  u5lemnab 636  u4lem1n 724  u3lem3n 736  u4lem5 746  u3lem10 767  u3lem11 768  u3lem11a 769  neg3antlem2 847  marsdenlem4 865  mlaconjo 868  oa4v3v 914

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

This theorem depends on definitions:  df-a 39

metamath.org