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  1531  norass  1538  cadan  1610  cadcomb  1614  nf2  1786  19.31v  1942  19.31  2241  2ralor  3210  eueq2  3668  uncom  4110  undif3  4252  reuun2  4277  dfif2  4481  reuprg  4660  rabrsn  4681  tppreqb  4761  ssunsn2  4783  disjor  5080  zfpair  5366  somin1  6090  ordtri2  6352  on0eqel  6442  fununi  6567  eliman0  6871  poxp2  8085  swoer  8666  supgtoreq  9374  cantnflem1d  9597  cantnflem1  9598  cflim2  10173  dffin7-2  10308  fpwwe2lem12  10553  suplem2pr  10964  leloe  11219  mulcan2g  11791  fimaxre  12086  fiminre  12089  arch  12398  elznn0nn  12502  elznn0  12503  nneo  12576  ltxr  13029  xrleloe  13058  xrrebnd  13083  xmullem2  13180  xmulcom  13181  xmulneg1  13184  xmulf  13187  sqeqori  14137  hashtpg  14408  odd2np1lem  16267  lcmcom  16520  dvdsprime  16614  coprm  16638  dvdszzq  16648  opprdomnb  20650  orngsqr  20799  lvecvscan2  21067  mplcoe1  21992  mplcoe5  21995  madutpos  22586  restntr  23126  alexsubALTlem2  23992  alexsubALTlem3  23993  xrsxmet  24754  dyaddisj  25553  mdegleb  26025  atandm3  26844  wilthlem2  27035  lgsdir2lem4  27295  noextenddif  27636  lesloe  27722  elzs2  28395  elznns  28398  tgcolg  28626  hlcomb  28675  axcontlem7  29043  elntg2  29058  nb3grprlem2  29454  vtxd0nedgb  29562  clwwlkneq0  30104  eupth2lem2  30294  eupth2lem3lem6  30308  numclwwlk3lem2lem  30458  hvmulcan2  31148  elat2  32415  chrelat2i  32440  atoml2i  32458  or3dir  32534  rmounid  32569  disjnf  32645  disjorf  32654  disjex  32667  disjexc  32668  disjunsn  32669  funcnv5mpt  32746  elicoelioo  32858  xrdifh  32860  tlt3  33052  ballotlemfc0  34650  ballotlemfcc  34651  bnj563  34899  subfacp1lem6  35379  dfon2lem5  35979  btwnconn1lem14  36294  outsideofcom  36322  outsideofeu  36325  lineunray  36341  ecase13d  36507  elicc3  36511  nn0prpw  36517  bj-dfbi5  36774  bj-consensusALT  36779  topdifinfeq  37551  onsucuni3  37568  wl-ifpimpr  37667  wl-cases2-dnf  37713  itg2addnclem2  37869  itgaddnclem2  37876  orfa  38279  notornotel2  38293  tsbi4  38333  ineleq  38543  disjecxrncnvep  38594  dfsucmap3  38633  leatb  39548  leat2  39550  isat3  39563  hlrelat2  39659  elpadd0  40065  aks6d1c2p2  42369  fsuppind  42829  safesnsupfilb  43655  ifporcor  43699  ifpim2  43709  ifpim23g  43732  ifpim123g  43737  rp-fakeoranass  43751  ontric3g  43759  stoweidlem26  46266  2reu3  47352  usgrexmpl2nb5  48278  itschlc0xyqsol1  49008  itschlc0xyqsol  49009  inlinecirc02plem  49028