Theorem orcom 866

Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)

Assertion

Ref	Expression
orcom	⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		pm1.4 865	. 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
2		pm1.4 865	. 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓))
3	1, 2	impbii 208	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 205   ∨ wo 843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 844

This theorem is referenced by:  orcomd  867  unitreslOLD  874  orbi1i  910  orbi1d  913  orass  918  or32  922  or42  924  pm5.7  950  oranabs  996  ordir  1003  pm5.17  1008  dn1  1054  dfifp7  1066  3orrot  1090  norcom  1524  norcomOLD  1525  norass  1535  cadan  1612  cadcomb  1616  nf2  1789  nfnbiOLD  1859  19.31v  1945  19.31  2230  2ralor  3294  eueq2  3640  uncom  4083  undif3  4221  reuun2  4245  dfif2  4458  reuprg  4636  rabrsn  4657  tppreqb  4735  ssunsn2  4757  dfopif  4797  disjor  5050  zfpair  5339  somin1  6027  ordtri2  6286  on0eqel  6369  fununi  6493  eliman0  6791  swoer  8486  supgtoreq  9159  cantnflem1d  9376  cantnflem1  9377  cflim2  9950  dffin7-2  10085  fpwwe2lem12  10329  suplem2pr  10740  leloe  10992  mulcan2g  11559  fimaxre  11849  fiminre  11852  arch  12160  elznn0nn  12263  elznn0  12264  nneo  12334  ltxr  12780  xrleloe  12807  xrrebnd  12831  xmullem2  12928  xmulcom  12929  xmulneg1  12932  xmulf  12935  sqeqori  13858  hashtpg  14127  odd2np1lem  15977  lcmcom  16226  dvdsprime  16320  coprm  16344  lvecvscan2  20289  opprdomn  20485  mplcoe1  21148  mplcoe5  21151  madutpos  21699  restntr  22241  alexsubALTlem2  23107  alexsubALTlem3  23108  xrsxmet  23878  dyaddisj  24665  mdegleb  25134  atandm3  25933  wilthlem2  26123  lgsdir2lem4  26381  tgcolg  26819  hlcomb  26868  axcontlem7  27241  elntg2  27256  nb3grprlem2  27651  vtxd0nedgb  27758  clwwlkneq0  28294  eupth2lem2  28484  eupth2lem3lem6  28498  numclwwlk3lem2lem  28648  hvmulcan2  29336  elat2  30603  chrelat2i  30628  atoml2i  30646  or3dir  30712  rmounid  30744  disjnf  30810  disjorf  30819  disjex  30832  disjexc  30833  disjunsn  30834  funcnv5mpt  30907  elicoelioo  31001  xrdifh  31003  dvdszzq  31031  tlt3  31150  orngsqr  31405  ballotlemfc0  32359  ballotlemfcc  32360  bnj563  32623  subfacp1lem6  33047  3orel2  33556  dfon2lem5  33669  poxp2  33717  noextenddif  33798  sleloe  33884  btwnconn1lem14  34329  outsideofcom  34357  outsideofeu  34360  lineunray  34376  ecase13d  34429  elicc3  34433  nn0prpw  34439  bj-dfbi5  34682  bj-consensusALT  34687  topdifinfeq  35448  onsucuni3  35465  wl-ifpimpr  35564  wl-cases2-dnf  35598  itg2addnclem2  35756  itgaddnclem2  35763  orfa  36167  notornotel2  36181  tsbi4  36221  ineleq  36413  leatb  37233  leat2  37235  isat3  37248  hlrelat2  37344  elpadd0  37750  fsuppind  40202  ifporcor  40967  ifpim2  40977  ifpim23g  41000  ifpim123g  41005  rp-fakeoranass  41019  ontric3g  41027  elprn2  43065  stoweidlem26  43457  2reu3  44489  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  inlinecirc02plem  46020