Theorem oran 87

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 30	. 2 (a'' v b'') = (a'' v b'')''
2		ax-a1 30	. . 3 a = a''
3		ax-a1 30	. . 3 b = b''
4	2, 3	2or 72	. 2 (a v b) = (a'' v b'')
5		df-a 40	. . 3 (a' ^ b') = (a'' v b'')'
6	5	ax-r4 37	. 2 (a' ^ b')' = (a'' v b'')''
7	1, 4, 6	3tr1 63	1 (a v b) = (a' ^ b')'

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

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 1052

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

Copyright terms: Public domain