Theorem orcom 870

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  orcomd  871  orbi1i  913  orbi1d  916  orass  921  or32  925  or42  927  biorfri  939  pm5.7  955  oranabs  1001  ordir  1008  pm5.17  1013  dn1  1057  dfifp7  1069  3orrot  1091  3orel2OLD  1487  norcom  1530  norass  1537  cadan  1609  cadcomb  1613  nf2  1785  19.31v  1941  19.31  2235  2ralor  3203  eueq2  3672  uncom  4111  undif3  4253  reuun2  4278  dfif2  4480  reuprg  4657  rabrsn  4678  tppreqb  4759  ssunsn2  4781  disjor  5077  zfpair  5363  somin1  6086  ordtri2  6346  on0eqel  6436  fununi  6561  eliman0  6864  poxp2  8083  swoer  8663  supgtoreq  9380  cantnflem1d  9603  cantnflem1  9604  cflim2  10176  dffin7-2  10311  fpwwe2lem12  10555  suplem2pr  10966  leloe  11220  mulcan2g  11792  fimaxre  12087  fiminre  12090  arch  12399  elznn0nn  12503  elznn0  12504  nneo  12578  ltxr  13035  xrleloe  13064  xrrebnd  13088  xmullem2  13185  xmulcom  13186  xmulneg1  13189  xmulf  13192  sqeqori  14139  hashtpg  14410  odd2np1lem  16269  lcmcom  16522  dvdsprime  16616  coprm  16640  dvdszzq  16650  opprdomnb  20620  orngsqr  20769  lvecvscan2  21037  mplcoe1  21960  mplcoe5  21963  madutpos  22545  restntr  23085  alexsubALTlem2  23951  alexsubALTlem3  23952  xrsxmet  24714  dyaddisj  25513  mdegleb  25985  atandm3  26804  wilthlem2  26995  lgsdir2lem4  27255  noextenddif  27596  sleloe  27682  elzs2  28310  elznns  28313  tgcolg  28517  hlcomb  28566  axcontlem7  28933  elntg2  28948  nb3grprlem2  29344  vtxd0nedgb  29452  clwwlkneq0  29991  eupth2lem2  30181  eupth2lem3lem6  30195  numclwwlk3lem2lem  30345  hvmulcan2  31035  elat2  32302  chrelat2i  32327  atoml2i  32345  or3dir  32422  rmounid  32457  disjnf  32532  disjorf  32541  disjex  32554  disjexc  32555  disjunsn  32556  funcnv5mpt  32625  elicoelioo  32734  xrdifh  32736  tlt3  32925  ballotlemfc0  34460  ballotlemfcc  34461  bnj563  34709  subfacp1lem6  35157  dfon2lem5  35760  btwnconn1lem14  36073  outsideofcom  36101  outsideofeu  36104  lineunray  36120  ecase13d  36286  elicc3  36290  nn0prpw  36296  bj-dfbi5  36547  bj-consensusALT  36552  topdifinfeq  37323  onsucuni3  37340  wl-ifpimpr  37439  wl-cases2-dnf  37485  itg2addnclem2  37651  itgaddnclem2  37658  orfa  38061  notornotel2  38075  tsbi4  38115  ineleq  38321  disjecxrncnvep  38361  leatb  39270  leat2  39272  isat3  39285  hlrelat2  39382  elpadd0  39788  aks6d1c2p2  42092  fsuppind  42563  safesnsupfilb  43391  ifporcor  43435  ifpim2  43445  ifpim23g  43468  ifpim123g  43473  rp-fakeoranass  43487  ontric3g  43495  elprn2  45616  stoweidlem26  46008  2reu3  47095  usgrexmpl2nb5  48021  itschlc0xyqsol1  48752  itschlc0xyqsol  48753  inlinecirc02plem  48772