Theorem oran 79

Description: Disjunction expressed with conjunction.

Assertion

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

Proof of Theorem oran

Step	Hyp	Ref	Expression
1		ax-a1 29	. 2 (a_|__|_ v b_|__|_) = (a_|__|_ v b_|__|_)_|__|_
2		ax-a1 29	. . 3 a = a_|__|_
3		ax-a1 29	. . 3 b = b_|__|_
4	2, 3	2or 67	. 2 (a v b) = (a_|__|_ v b_|__|_)
5		df-a 39	. . 3 (a_|_ ^ b_|_) = (a_|__|_ v b_|__|_)_|_
6	5	ax-r4 36	. 2 (a_|_ ^ b_|_)_|_ = (a_|__|_ v b_|__|_)_|__|_
7	1, 4, 6	3tr1 60	1 (a v b) = (a_|_ ^ b_|_)_|_

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

This theorem is referenced by:  anor3 82  dfb 86  dfnb 87  mi 117  lecon 146  wlem3.1 202  wwcomd 206  wwfh1 208  wwfh2 209  wwfh3 210  wwfh4 211  ska2b 219  ka4lemo 220  ska10 230  ni31 242  ud2lem0c 270  ud4lem0c 272  ud5lem0c 273  nom12 301  nom13 302  2vwomlem 347  wlecon 377  wcomd 400  wcomdr 403  wfh1 405  wfh2 406  wfh3 407  wfh4 408  ska2 414  ska4 415  wom2 416  lem3.1 425  comd 438  comdr 448  fh1 451  fh2 452  fh3 453  fh4 454  i3bi 478  ni32 484  lem4 493  i3orlem5 538  ud1lem2 543  ud2lem1 545  ud2lem2 546  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem2 553  ud3lem3d 557  ud4lem1a 559  ud4lem2 564  ud5lem1b 569  ud5lem1 571  ud5lem3c 575  u2lemoa 603  u3lemob 614  u3lemnana 629  u5lemnana 631  u1lemnanb 637  u2lemnanb 638  u3lemnanb 639  u4lemnanb 640  u5lemnanb 641  u2lem1 717  u4lem1n 724  u3lem11 768  u3lem15 777  1oa 802  2oalem1 807  2oath1 808  bi3 821  mlaconj4 826  mlaconjo 868  mhcor1 870  oa6fromdual 933

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