Theorem orcom 884

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orcomd  885  orbi1i  927  orbi1d  930  orass  935  or32  939  or42  941  biorfri  953  pm5.7  968  oranabs  1015  ordir  1024  pm5.17  1029  dn1  1073  dfifp7  1085  3orrot  1108  3orel2OLD  1516  norcom  1560  norass  1567  cadan  1642  cadcomb  1646  nf2  1818  19.31v  1974  19.31  2271  2ralor  3237  eueq2  3668  uncom  4105  undif3  4246  reuun2  4271  dfif2  4484  reuprg  4664  rabrsn  4685  tppreqb  4768  ssunsn2  4788  disjor  5085  zfpair  5383  somin1  6125  ordtri2  6391  on0eqel  6481  fununi  6607  eliman0  6914  poxp2  8144  swoer  8733  supgtoreq  9447  cantnflem1d  9673  cantnflem1  9674  cflim2  10322  dffin7-2  10457  fpwwe2lem12  10708  suplem2pr  11119  leloe  11377  mulcan2g  11951  fimaxre  12242  fiminre  12245  arch  12584  elznn0nn  12688  elznn0  12689  nneo  12764  ltxr  13225  xrleloe  13254  xrrebnd  13279  xmullem2  13376  xmulcom  13377  xmulneg1  13380  xmulf  13383  sqeqori  14338  hashtpg  14610  odd2np1lem  16490  lcmcom  16748  dvdsprime  16842  coprm  16867  dvdszzq  16877  opprdomnb  20948  orngsqr  21103  lvecvscan2  21370  mplcoe1  22326  mplcoe5  22329  madutpos  22937  restntr  23480  alexsubALTlem2  24347  alexsubALTlem3  24348  xrsxmet  25109  dyaddisj  25897  mdegleb  26362  atandm3  27188  wilthlem2  27378  lgsdir2lem4  27637  noextenddif  28007  lesloe  28093  elzs2  28767  elznns  28770  tgcolg  28999  hlcomb  29051  plngcplem  29245  plngrotlem2  29248  axcontlem7  29530  elntg2  29545  nb3grprlem2  29944  vtxd0nedgb  30051  clwwlkneq0  30602  eupth2lem2  30802  eupth2lem3lem6  30816  numclwwlk3lem2lem  30966  hvmulcan2  31657  elat2  32924  chrelat2i  32949  atoml2i  32967  or3dir  33040  rmounid  33073  disjnf  33146  disjorf  33155  disjex  33168  disjexc  33169  disjunsn  33170  funcnv5mpt  33243  elicoelioo  33352  xrdifh  33354  tlt3  33513  ballotlemfc0  35108  ballotlemfcc  35109  bnj563  35357  subfacp1lem6  35919  dfon2lem5  36519  btwnconn1lem14  36835  outsideofcom  36863  outsideofeu  36866  lineunray  36882  ltnadd  36937  elicc3  37075  nn0prpw  37081  bj-dfbi5  37414  bj-consensusALT  37419  topdifinfeq  38241  onsucuni3  38258  wl-ifpimpr  38357  wl-cases2-dnf  38412  itg2addnclem2  38558  itgaddnclem2  38565  orfa  38984  notornotel2  38996  tsbi4  39036  ineleq  39254  disjecxrncnvep  39313  dfsucmap3  39363  dfdisjALTV5a  39703  dfeldisj5a  39714  leatb  40317  leat2  40319  isat3  40332  hlrelat2  40428  elpadd0  40834  aks6d1c2p2  43137  fsuppind  43580  safesnsupfilb  44377  ifporcor  44421  ifpim2  44431  ifpim23g  44454  ifpim123g  44459  rp-fakeoranass  44473  ontric3g  44481  stoweidlem26  46980  goldratmolem4  47879  2reu3  48124  usgrexmpl2nb5  49078  itschlc0xyqsol1  49822  itschlc0xyqsol  49823  inlinecirc02plem  49842