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  1486  norcom  1529  norass  1536  cadan  1608  cadcomb  1612  nf2  1784  19.31v  1940  19.31  2233  2ralor  3218  eueq2  3700  uncom  4140  undif3  4282  reuun2  4307  dfif2  4509  reuprg  4685  rabrsn  4706  tppreqb  4787  ssunsn2  4809  disjor  5107  zfpair  5403  somin1  6135  ordtri2  6400  on0eqel  6489  fununi  6622  eliman0  6927  poxp2  8151  swoer  8759  supgtoreq  9493  cantnflem1d  9711  cantnflem1  9712  cflim2  10286  dffin7-2  10421  fpwwe2lem12  10665  suplem2pr  11076  leloe  11330  mulcan2g  11900  fimaxre  12195  fiminre  12198  arch  12507  elznn0nn  12611  elznn0  12612  nneo  12686  ltxr  13140  xrleloe  13169  xrrebnd  13193  xmullem2  13290  xmulcom  13291  xmulneg1  13294  xmulf  13297  sqeqori  14236  hashtpg  14507  odd2np1lem  16360  lcmcom  16613  dvdsprime  16707  coprm  16731  dvdszzq  16741  opprdomnb  20690  lvecvscan2  21087  mplcoe1  22022  mplcoe5  22025  madutpos  22615  restntr  23155  alexsubALTlem2  24021  alexsubALTlem3  24022  xrsxmet  24786  dyaddisj  25586  mdegleb  26058  atandm3  26876  wilthlem2  27067  lgsdir2lem4  27327  noextenddif  27668  sleloe  27754  elzs2  28340  elznns  28343  tgcolg  28517  hlcomb  28566  axcontlem7  28934  elntg2  28949  nb3grprlem2  29345  vtxd0nedgb  29453  clwwlkneq0  29995  eupth2lem2  30185  eupth2lem3lem6  30199  numclwwlk3lem2lem  30349  hvmulcan2  31039  elat2  32306  chrelat2i  32331  atoml2i  32349  or3dir  32426  rmounid  32461  disjnf  32530  disjorf  32539  disjex  32552  disjexc  32553  disjunsn  32554  funcnv5mpt  32625  elicoelioo  32727  xrdifh  32729  tlt3  32906  orngsqr  33280  ballotlemfc0  34436  ballotlemfcc  34437  bnj563  34698  subfacp1lem6  35131  dfon2lem5  35729  btwnconn1lem14  36042  outsideofcom  36070  outsideofeu  36073  lineunray  36089  ecase13d  36255  elicc3  36259  nn0prpw  36265  bj-dfbi5  36516  bj-consensusALT  36521  topdifinfeq  37292  onsucuni3  37309  wl-ifpimpr  37408  wl-cases2-dnf  37454  itg2addnclem2  37620  itgaddnclem2  37627  orfa  38030  notornotel2  38044  tsbi4  38084  ineleq  38296  disjecxrncnvep  38332  leatb  39234  leat2  39236  isat3  39249  hlrelat2  39346  elpadd0  39752  aks6d1c2p2  42061  fsuppind  42545  safesnsupfilb  43376  ifporcor  43420  ifpim2  43430  ifpim23g  43453  ifpim123g  43458  rp-fakeoranass  43472  ontric3g  43480  elprn2  45594  stoweidlem26  45986  2reu3  47068  usgrexmpl2nb5  47941  itschlc0xyqsol1  48633  itschlc0xyqsol  48634  inlinecirc02plem  48653