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 211	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 208   ∨ 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 209  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  1052  dfifp7  1064  3orrot  1088  norcom  1522  norcomOLD  1523  norass  1533  cadan  1610  cadcomb  1614  nf2  1786  nfnbi  1855  19.31v  1942  19.31  2236  r19.30OLD  3339  eueq2  3701  uncom  4129  undif3  4265  reuun2  4286  dfif2  4469  reuprg  4639  rabrsn  4660  tppreqb  4738  ssunsn2  4760  disjor  5046  zfpair  5322  somin1  5993  ordtri2  6226  on0eqel  6308  fununi  6429  eliman0  6705  swoer  8319  supgtoreq  8934  cantnflem1d  9151  cantnflem1  9152  cflim2  9685  dffin7-2  9820  fpwwe2lem13  10064  suplem2pr  10475  leloe  10727  mulcan2g  11294  fimaxre  11584  fimaxreOLD  11585  fiminre  11588  arch  11895  elznn0nn  11996  elznn0  11997  nneo  12067  ltxr  12511  xrleloe  12538  xrrebnd  12562  xmullem2  12659  xmulcom  12660  xmulneg1  12663  xmulf  12666  sqeqori  13577  hashtpg  13844  odd2np1lem  15689  lcmcom  15937  dvdsprime  16031  coprm  16055  lvecvscan2  19884  opprdomn  20074  mplcoe1  20246  mplcoe5  20249  madutpos  21251  restntr  21790  alexsubALTlem2  22656  alexsubALTlem3  22657  xrsxmet  23417  dyaddisj  24197  mdegleb  24658  atandm3  25456  wilthlem2  25646  lgsdir2lem4  25904  tgcolg  26340  hlcomb  26389  axcontlem7  26756  elntg2  26771  nb3grprlem2  27163  vtxd0nedgb  27270  clwwlkneq0  27807  eupth2lem2  27998  eupth2lem3lem6  28012  numclwwlk3lem2lem  28162  hvmulcan2  28850  elat2  30117  chrelat2i  30142  atoml2i  30160  or3dir  30226  rmounid  30259  disjnf  30320  disjorf  30329  disjex  30342  disjexc  30343  disjunsn  30344  funcnv5mpt  30413  elicoelioo  30501  xrdifh  30503  dvdszzq  30531  tlt3  30652  orngsqr  30877  ballotlemfc0  31750  ballotlemfcc  31751  bnj563  32014  subfacp1lem6  32432  3orel2  32941  dfon2lem5  33032  noextenddif  33175  sleloe  33233  btwnconn1lem14  33561  outsideofcom  33589  outsideofeu  33592  lineunray  33608  ecase13d  33661  elicc3  33665  nn0prpw  33671  bj-dfbi5  33907  bj-consensusALT  33912  topdifinfeq  34634  onsucuni3  34651  wl-cases2-dnf  34767  itg2addnclem2  34959  itgaddnclem2  34966  orfa  35375  notornotel2  35389  tsbi4  35429  ineleq  35623  leatb  36443  leat2  36445  isat3  36458  hlrelat2  36554  elpadd0  36960  ifporcor  39847  ifpim2  39857  ifpim23g  39881  ifpim123g  39886  rp-fakeoranass  39900  ontric3g  39908  elprn2  41935  stoweidlem26  42331  2reu3  43329  itschlc0xyqsol1  44773  itschlc0xyqsol  44774  inlinecirc02plem  44793