Theorem orcom 867

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

Syntax hints:   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orcomd  868  unitreslOLD  875  orbi1i  911  orbi1d  914  orass  919  or32  923  or42  925  pm5.7  951  oranabs  997  ordir  1004  pm5.17  1009  dn1  1053  dfifp7  1065  3orrot  1089  norcom  1523  norcomOLD  1524  norass  1534  cadan  1611  cadcomb  1615  nf2  1787  nfnbi  1856  19.31v  1942  19.31  2234  eueq2  3649  uncom  4080  undif3  4215  reuun2  4238  dfif2  4427  reuprg  4599  rabrsn  4620  tppreqb  4698  ssunsn2  4720  disjor  5010  zfpair  5287  somin1  5960  ordtri2  6194  on0eqel  6276  fununi  6399  eliman0  6680  swoer  8302  supgtoreq  8918  cantnflem1d  9135  cantnflem1  9136  cflim2  9674  dffin7-2  9809  fpwwe2lem13  10053  suplem2pr  10464  leloe  10716  mulcan2g  11283  fimaxre  11573  fiminre  11576  arch  11882  elznn0nn  11983  elznn0  11984  nneo  12054  ltxr  12498  xrleloe  12525  xrrebnd  12549  xmullem2  12646  xmulcom  12647  xmulneg1  12650  xmulf  12653  sqeqori  13572  hashtpg  13839  odd2np1lem  15681  lcmcom  15927  dvdsprime  16021  coprm  16045  lvecvscan2  19877  opprdomn  20067  mplcoe1  20705  mplcoe5  20708  madutpos  21247  restntr  21787  alexsubALTlem2  22653  alexsubALTlem3  22654  xrsxmet  23414  dyaddisj  24200  mdegleb  24665  atandm3  25464  wilthlem2  25654  lgsdir2lem4  25912  tgcolg  26348  hlcomb  26397  axcontlem7  26764  elntg2  26779  nb3grprlem2  27171  vtxd0nedgb  27278  clwwlkneq0  27814  eupth2lem2  28004  eupth2lem3lem6  28018  numclwwlk3lem2lem  28168  hvmulcan2  28856  elat2  30123  chrelat2i  30148  atoml2i  30166  or3dir  30232  rmounid  30266  disjnf  30333  disjorf  30342  disjex  30355  disjexc  30356  disjunsn  30357  funcnv5mpt  30431  elicoelioo  30527  xrdifh  30529  dvdszzq  30557  tlt3  30678  orngsqr  30928  ballotlemfc0  31860  ballotlemfcc  31861  bnj563  32124  subfacp1lem6  32545  3orel2  33054  dfon2lem5  33145  noextenddif  33288  sleloe  33346  btwnconn1lem14  33674  outsideofcom  33702  outsideofeu  33705  lineunray  33721  ecase13d  33774  elicc3  33778  nn0prpw  33784  bj-dfbi5  34020  bj-consensusALT  34025  topdifinfeq  34767  onsucuni3  34784  wl-ifpimpr  34883  wl-cases2-dnf  34917  itg2addnclem2  35109  itgaddnclem2  35116  orfa  35520  notornotel2  35534  tsbi4  35574  ineleq  35768  leatb  36588  leat2  36590  isat3  36603  hlrelat2  36699  elpadd0  37105  fsuppind  39456  ifporcor  40170  ifpim2  40180  ifpim23g  40203  ifpim123g  40208  rp-fakeoranass  40222  ontric3g  40230  elprn2  42276  stoweidlem26  42668  2reu3  43666  itschlc0xyqsol1  45180  itschlc0xyqsol  45181  inlinecirc02plem  45200