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  3211  eueq2  3656  uncom  4098  undif3  4240  reuun2  4265  dfif2  4468  reuprg  4647  rabrsn  4668  tppreqb  4750  ssunsn2  4770  disjor  5067  zfpair  5363  somin1  6096  ordtri2  6358  on0eqel  6448  fununi  6573  eliman0  6877  poxp2  8093  swoer  8675  supgtoreq  9384  cantnflem1d  9609  cantnflem1  9610  cflim2  10185  dffin7-2  10320  fpwwe2lem12  10565  suplem2pr  10976  leloe  11232  mulcan2g  11804  fimaxre  12100  fiminre  12103  arch  12434  elznn0nn  12538  elznn0  12539  nneo  12613  ltxr  13066  xrleloe  13095  xrrebnd  13120  xmullem2  13217  xmulcom  13218  xmulneg1  13221  xmulf  13224  sqeqori  14176  hashtpg  14447  odd2np1lem  16309  lcmcom  16562  dvdsprime  16656  coprm  16681  dvdszzq  16691  opprdomnb  20694  orngsqr  20843  lvecvscan2  21110  mplcoe1  22015  mplcoe5  22018  madutpos  22607  restntr  23147  alexsubALTlem2  24013  alexsubALTlem3  24014  xrsxmet  24775  dyaddisj  25563  mdegleb  26029  atandm3  26842  wilthlem2  27032  lgsdir2lem4  27291  noextenddif  27632  lesloe  27718  elzs2  28391  elznns  28394  tgcolg  28622  hlcomb  28671  axcontlem7  29039  elntg2  29054  nb3grprlem2  29450  vtxd0nedgb  29557  clwwlkneq0  30099  eupth2lem2  30289  eupth2lem3lem6  30303  numclwwlk3lem2lem  30453  hvmulcan2  31144  elat2  32411  chrelat2i  32436  atoml2i  32454  or3dir  32529  rmounid  32564  disjnf  32640  disjorf  32649  disjex  32662  disjexc  32663  disjunsn  32664  funcnv5mpt  32740  elicoelioo  32851  xrdifh  32853  tlt3  33030  ballotlemfc0  34637  ballotlemfcc  34638  bnj563  34886  subfacp1lem6  35367  dfon2lem5  35967  btwnconn1lem14  36282  outsideofcom  36310  outsideofeu  36313  lineunray  36329  ecase13d  36495  elicc3  36499  nn0prpw  36505  bj-dfbi5  36839  bj-consensusALT  36844  topdifinfeq  37666  onsucuni3  37683  wl-ifpimpr  37782  wl-cases2-dnf  37837  itg2addnclem2  37993  itgaddnclem2  38000  orfa  38403  notornotel2  38417  tsbi4  38457  ineleq  38675  disjecxrncnvep  38734  dfsucmap3  38784  dfdisjALTV5a  39124  dfeldisj5a  39135  leatb  39738  leat2  39740  isat3  39753  hlrelat2  39849  elpadd0  40255  aks6d1c2p2  42558  fsuppind  43023  safesnsupfilb  43845  ifporcor  43889  ifpim2  43899  ifpim23g  43922  ifpim123g  43927  rp-fakeoranass  43941  ontric3g  43949  stoweidlem26  46454  2reu3  47558  usgrexmpl2nb5  48512  itschlc0xyqsol1  49242  itschlc0xyqsol  49243  inlinecirc02plem  49262