Theorem oran 87

Description: Disjunction expressed with conjunction. (Contributed by NM, 10-Aug-1997.)

Assertion

Ref	Expression
oran	(a ∪ b) = (a⊥ ∩ b⊥ )⊥

Proof of Theorem oran

Step	Hyp	Ref	Expression
1		ax-a1 30	. 2 (a⊥ ⊥ ∪ b⊥ ⊥ ) = (a⊥ ⊥ ∪ b⊥ ⊥ )⊥ ⊥
2		ax-a1 30	. . 3 a = a⊥ ⊥
3		ax-a1 30	. . 3 b = b⊥ ⊥
4	2, 3	2or 72	. 2 (a ∪ b) = (a⊥ ⊥ ∪ b⊥ ⊥ )
5		df-a 40	. . 3 (a⊥ ∩ b⊥ ) = (a⊥ ⊥ ∪ b⊥ ⊥ )⊥
6	5	ax-r4 37	. 2 (a⊥ ∩ b⊥ )⊥ = (a⊥ ⊥ ∪ b⊥ ⊥ )⊥ ⊥
7	1, 4, 6	3tr1 63	1 (a ∪ b) = (a⊥ ∩ b⊥ )⊥

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

This theorem depends on definitions:  df-a 40

This theorem is referenced by:  anor3  90  dfb  94  dfnb  95  mi  125  lecon  154  wlem3.1  210  wwcomd  214  wwfh1  216  wwfh2  217  wwfh3  218  wwfh4  219  ska2b  227  ka4lemo  228  ska10  238  ni31  250  ud2lem0c  278  ud4lem0c  280  ud5lem0c  281  nom12  309  nom13  310  2vwomlem  365  wlecon  395  wcomd  418  wcomdr  421  wfh1  423  wfh2  424  wfh3  425  wfh4  426  ska2  432  ska4  433  wom2  434  comd  456  comdr  466  fh1  469  fh2  470  fh3  471  fh4  472  i3bi  496  ni32  502  lem4  511  i3orlem5  556  ud1lem2  561  ud2lem1  563  ud2lem2  564  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem2  571  ud3lem3d  575  ud4lem1a  577  ud4lem2  582  ud5lem1b  587  ud5lem1  589  ud5lem3c  593  u2lemoa  621  u3lemob  632  u3lemnana  647  u5lemnana  649  u1lemnanb  655  u2lemnanb  656  u3lemnanb  657  u4lemnanb  658  u5lemnanb  659  u2lem1  735  u4lem1n  742  u3lem11  786  u3lem15  795  1oa  820  2oalem1  825  2oath1  826  bi3  839  mlaconj4  844  mlaconjo  886  mhcor1  888  oa6fromdual  953  lem3.3.4  1053