Theorem orcom 869

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

Syntax hints:   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  orcomd  870  orbi1i  912  orbi1d  915  orass  920  or32  924  or42  926  biorfri  938  pm5.7  954  oranabs  1000  ordir  1007  pm5.17  1012  dn1  1058  dfifp7  1070  3orrot  1092  3orel2  1484  norcom  1527  norass  1534  cadan  1606  cadcomb  1610  nf2  1783  nfnbiOLD  1854  19.31v  1940  19.31  2235  2ralor  3237  eueq2  3732  uncom  4181  undif3  4319  reuun2  4344  dfif2  4550  reuprg  4728  rabrsn  4749  tppreqb  4830  ssunsn2  4852  disjor  5148  zfpair  5439  somin1  6165  ordtri2  6430  on0eqel  6519  fununi  6653  eliman0  6960  poxp2  8184  swoer  8794  supgtoreq  9539  cantnflem1d  9757  cantnflem1  9758  cflim2  10332  dffin7-2  10467  fpwwe2lem12  10711  suplem2pr  11122  leloe  11376  mulcan2g  11944  fimaxre  12239  fiminre  12242  arch  12550  elznn0nn  12653  elznn0  12654  nneo  12727  ltxr  13178  xrleloe  13206  xrrebnd  13230  xmullem2  13327  xmulcom  13328  xmulneg1  13331  xmulf  13334  sqeqori  14263  hashtpg  14534  odd2np1lem  16388  lcmcom  16640  dvdsprime  16734  coprm  16758  dvdszzq  16768  opprdomnb  20739  lvecvscan2  21137  mplcoe1  22078  mplcoe5  22081  madutpos  22669  restntr  23211  alexsubALTlem2  24077  alexsubALTlem3  24078  xrsxmet  24850  dyaddisj  25650  mdegleb  26123  atandm3  26939  wilthlem2  27130  lgsdir2lem4  27390  noextenddif  27731  sleloe  27817  elzs2  28403  elznns  28406  tgcolg  28580  hlcomb  28629  axcontlem7  29003  elntg2  29018  nb3grprlem2  29416  vtxd0nedgb  29524  clwwlkneq0  30061  eupth2lem2  30251  eupth2lem3lem6  30265  numclwwlk3lem2lem  30415  hvmulcan2  31105  elat2  32372  chrelat2i  32397  atoml2i  32415  or3dir  32489  rmounid  32523  disjnf  32592  disjorf  32601  disjex  32614  disjexc  32615  disjunsn  32616  funcnv5mpt  32686  elicoelioo  32783  xrdifh  32785  tlt3  32943  orngsqr  33299  ballotlemfc0  34457  ballotlemfcc  34458  bnj563  34719  subfacp1lem6  35153  dfon2lem5  35751  btwnconn1lem14  36064  outsideofcom  36092  outsideofeu  36095  lineunray  36111  ecase13d  36279  elicc3  36283  nn0prpw  36289  bj-dfbi5  36540  bj-consensusALT  36545  topdifinfeq  37316  onsucuni3  37333  wl-ifpimpr  37432  wl-cases2-dnf  37466  itg2addnclem2  37632  itgaddnclem2  37639  orfa  38042  notornotel2  38056  tsbi4  38096  ineleq  38310  disjecxrncnvep  38346  leatb  39248  leat2  39250  isat3  39263  hlrelat2  39360  elpadd0  39766  aks6d1c2p2  42076  fsuppind  42545  safesnsupfilb  43380  ifporcor  43424  ifpim2  43434  ifpim23g  43457  ifpim123g  43462  rp-fakeoranass  43476  ontric3g  43484  elprn2  45555  stoweidlem26  45947  2reu3  47025  usgrexmpl2nb5  47851  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  inlinecirc02plem  48520