Theorem orcom 868

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 867	. 2 ⊢ ((𝜑 ∨ 𝜓) → (𝜓 ∨ 𝜑))
2		pm1.4 867	. 2 ⊢ ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 209   ∨ wo 845

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 210  df-or 846

This theorem is referenced by:  orcomd  869  unitreslOLD  876  orbi1i  912  orbi1d  915  orass  920  or32  924  or42  926  pm5.7  952  oranabs  998  ordir  1005  pm5.17  1010  dn1  1054  dfifp7  1066  3orrot  1090  norcom  1524  norcomOLD  1525  norass  1535  cadan  1612  cadcomb  1616  nf2  1788  nfnbi  1857  19.31v  1943  19.31  2235  eueq2  3621  uncom  4054  undif3  4191  reuun2  4216  dfif2  4415  reuprg  4589  rabrsn  4610  tppreqb  4688  ssunsn2  4710  dfopif  4750  disjor  5005  zfpair  5283  somin1  5958  ordtri2  6197  on0eqel  6280  fununi  6403  eliman0  6686  swoer  8322  supgtoreq  8952  cantnflem1d  9169  cantnflem1  9170  cflim2  9708  dffin7-2  9843  fpwwe2lem12  10087  suplem2pr  10498  leloe  10750  mulcan2g  11317  fimaxre  11607  fiminre  11610  arch  11916  elznn0nn  12019  elznn0  12020  nneo  12090  ltxr  12536  xrleloe  12563  xrrebnd  12587  xmullem2  12684  xmulcom  12685  xmulneg1  12688  xmulf  12691  sqeqori  13611  hashtpg  13880  odd2np1lem  15726  lcmcom  15974  dvdsprime  16068  coprm  16092  lvecvscan2  19937  opprdomn  20127  mplcoe1  20782  mplcoe5  20785  madutpos  21327  restntr  21867  alexsubALTlem2  22733  alexsubALTlem3  22734  xrsxmet  23495  dyaddisj  24281  mdegleb  24749  atandm3  25548  wilthlem2  25738  lgsdir2lem4  25996  tgcolg  26432  hlcomb  26481  axcontlem7  26848  elntg2  26863  nb3grprlem2  27255  vtxd0nedgb  27362  clwwlkneq0  27898  eupth2lem2  28088  eupth2lem3lem6  28102  numclwwlk3lem2lem  28252  hvmulcan2  28940  elat2  30207  chrelat2i  30232  atoml2i  30250  or3dir  30316  rmounid  30350  disjnf  30416  disjorf  30425  disjex  30438  disjexc  30439  disjunsn  30440  funcnv5mpt  30514  elicoelioo  30608  xrdifh  30610  dvdszzq  30638  tlt3  30759  orngsqr  31014  ballotlemfc0  31963  ballotlemfcc  31964  bnj563  32227  subfacp1lem6  32648  3orel2  33157  dfon2lem5  33264  poxp2  33330  noextenddif  33421  sleloe  33507  btwnconn1lem14  33936  outsideofcom  33964  outsideofeu  33967  lineunray  33983  ecase13d  34036  elicc3  34040  nn0prpw  34046  bj-dfbi5  34286  bj-consensusALT  34291  topdifinfeq  35032  onsucuni3  35049  wl-ifpimpr  35148  wl-cases2-dnf  35182  itg2addnclem2  35374  itgaddnclem2  35381  orfa  35785  notornotel2  35799  tsbi4  35839  ineleq  36033  leatb  36853  leat2  36855  isat3  36868  hlrelat2  36964  elpadd0  37370  fsuppind  39769  ifporcor  40528  ifpim2  40538  ifpim23g  40561  ifpim123g  40566  rp-fakeoranass  40580  ontric3g  40588  elprn2  42627  stoweidlem26  43019  2reu3  44019  itschlc0xyqsol1  45530  itschlc0xyqsol  45531  inlinecirc02plem  45550