Theorem orcom 881

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

Syntax hints:   ↔ wb 208   ∨ wo 858

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 859

This theorem is referenced by:  orcomd  882  orbi1i  924  orbi1d  927  orass  932  or32  936  or42  938  biorfri  950  pm5.7  966  oranabs  1012  ordir  1019  pm5.17  1024  dn1  1068  dfifp7  1080  3orrot  1102  3orel2OLD  1505  norcom  1549  norass  1556  cadan  1628  cadcomb  1632  nf2  1804  19.31v  1960  19.31  2268  2ralor  3235  eueq2  3672  uncom  4111  undif3  4252  reuun2  4277  dfif2  4481  reuprg  4661  rabrsn  4682  tppreqb  4764  ssunsn2  4784  disjor  5081  zfpair  5377  somin1  6117  ordtri2  6377  on0eqel  6467  fununi  6592  eliman0  6900  poxp2  8118  swoer  8705  supgtoreq  9414  cantnflem1d  9640  cantnflem1  9641  cflim2  10217  dffin7-2  10352  fpwwe2lem12  10597  suplem2pr  11008  leloe  11266  mulcan2g  11838  fimaxre  12133  fiminre  12136  arch  12475  elznn0nn  12579  elznn0  12580  nneo  12654  ltxr  13114  xrleloe  13143  xrrebnd  13168  xmullem2  13265  xmulcom  13266  xmulneg1  13269  xmulf  13272  sqeqori  14224  hashtpg  14495  odd2np1lem  16357  lcmcom  16610  dvdsprime  16704  coprm  16729  dvdszzq  16739  opprdomnb  20746  orngsqr  20895  lvecvscan2  21162  mplcoe1  22070  mplcoe5  22073  madutpos  22682  restntr  23222  alexsubALTlem2  24088  alexsubALTlem3  24089  xrsxmet  24850  dyaddisj  25638  mdegleb  26104  atandm3  26920  wilthlem2  27110  lgsdir2lem4  27369  noextenddif  27709  lesloe  27795  elzs2  28469  elznns  28472  tgcolg  28700  hlcomb  28749  axcontlem7  29117  elntg2  29132  nb3grprlem2  29528  vtxd0nedgb  29635  clwwlkneq0  30177  eupth2lem2  30367  eupth2lem3lem6  30381  numclwwlk3lem2lem  30531  hvmulcan2  31222  elat2  32489  chrelat2i  32514  atoml2i  32532  or3dir  32607  rmounid  32642  disjnf  32719  disjorf  32728  disjex  32741  disjexc  32742  disjunsn  32743  funcnv5mpt  32819  elicoelioo  32930  xrdifh  32932  tlt3  33109  ballotlemfc0  34751  ballotlemfcc  34752  bnj563  35003  subfacp1lem6  35499  dfon2lem5  36099  btwnconn1lem14  36414  outsideofcom  36442  outsideofeu  36445  lineunray  36461  ecase13d  36637  elicc3  36641  nn0prpw  36647  bj-dfbi5  36981  bj-consensusALT  36986  topdifinfeq  37808  onsucuni3  37825  wl-ifpimpr  37924  wl-cases2-dnf  37979  itg2addnclem2  38135  itgaddnclem2  38142  orfa  38545  notornotel2  38559  tsbi4  38599  ineleq  38817  disjecxrncnvep  38876  dfsucmap3  38926  dfdisjALTV5a  39266  dfeldisj5a  39277  leatb  39880  leat2  39882  isat3  39895  hlrelat2  39991  elpadd0  40397  aks6d1c2p2  42700  fsuppind  43136  safesnsupfilb  43958  ifporcor  44002  ifpim2  44012  ifpim23g  44035  ifpim123g  44040  rp-fakeoranass  44054  ontric3g  44062  stoweidlem26  46564  2reu3  47668  usgrexmpl2nb5  48622  itschlc0xyqsol1  49352  itschlc0xyqsol  49353  inlinecirc02plem  49372