Theorem orcom 871

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  orcomd  872  orbi1i  914  orbi1d  917  orass  922  or32  926  or42  928  biorfri  940  pm5.7  956  oranabs  1002  ordir  1009  pm5.17  1014  dn1  1058  dfifp7  1070  3orrot  1092  3orel2OLD  1488  norcom  1532  norass  1539  cadan  1611  cadcomb  1615  nf2  1787  19.31v  1943  19.31  2242  2ralor  3212  eueq2  3657  uncom  4099  undif3  4241  reuun2  4266  dfif2  4469  reuprg  4648  rabrsn  4669  tppreqb  4749  ssunsn2  4771  disjor  5068  zfpair  5358  somin1  6090  ordtri2  6352  on0eqel  6442  fununi  6567  eliman0  6871  poxp2  8086  swoer  8668  supgtoreq  9377  cantnflem1d  9600  cantnflem1  9601  cflim2  10176  dffin7-2  10311  fpwwe2lem12  10556  suplem2pr  10967  leloe  11223  mulcan2g  11795  fimaxre  12091  fiminre  12094  arch  12425  elznn0nn  12529  elznn0  12530  nneo  12604  ltxr  13057  xrleloe  13086  xrrebnd  13111  xmullem2  13208  xmulcom  13209  xmulneg1  13212  xmulf  13215  sqeqori  14167  hashtpg  14438  odd2np1lem  16300  lcmcom  16553  dvdsprime  16647  coprm  16672  dvdszzq  16682  opprdomnb  20685  orngsqr  20834  lvecvscan2  21102  mplcoe1  22025  mplcoe5  22028  madutpos  22617  restntr  23157  alexsubALTlem2  24023  alexsubALTlem3  24024  xrsxmet  24785  dyaddisj  25573  mdegleb  26039  atandm3  26855  wilthlem2  27046  lgsdir2lem4  27305  noextenddif  27646  lesloe  27732  elzs2  28405  elznns  28408  tgcolg  28636  hlcomb  28685  axcontlem7  29053  elntg2  29068  nb3grprlem2  29464  vtxd0nedgb  29572  clwwlkneq0  30114  eupth2lem2  30304  eupth2lem3lem6  30318  numclwwlk3lem2lem  30468  hvmulcan2  31159  elat2  32426  chrelat2i  32451  atoml2i  32469  or3dir  32544  rmounid  32579  disjnf  32655  disjorf  32664  disjex  32677  disjexc  32678  disjunsn  32679  funcnv5mpt  32755  elicoelioo  32866  xrdifh  32868  tlt3  33045  ballotlemfc0  34653  ballotlemfcc  34654  bnj563  34902  subfacp1lem6  35383  dfon2lem5  35983  btwnconn1lem14  36298  outsideofcom  36326  outsideofeu  36329  lineunray  36345  ecase13d  36511  elicc3  36515  nn0prpw  36521  bj-dfbi5  36855  bj-consensusALT  36860  topdifinfeq  37680  onsucuni3  37697  wl-ifpimpr  37796  wl-cases2-dnf  37851  itg2addnclem2  38007  itgaddnclem2  38014  orfa  38417  notornotel2  38431  tsbi4  38471  ineleq  38689  disjecxrncnvep  38748  dfsucmap3  38798  dfdisjALTV5a  39138  dfeldisj5a  39149  leatb  39752  leat2  39754  isat3  39767  hlrelat2  39863  elpadd0  40269  aks6d1c2p2  42572  fsuppind  43037  safesnsupfilb  43863  ifporcor  43907  ifpim2  43917  ifpim23g  43940  ifpim123g  43945  rp-fakeoranass  43959  ontric3g  43967  stoweidlem26  46472  2reu3  47570  usgrexmpl2nb5  48524  itschlc0xyqsol1  49254  itschlc0xyqsol  49255  inlinecirc02plem  49274