Theorem orcom 866

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

Syntax hints:   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  orcomd  867  unitreslOLD  874  orbi1i  910  orbi1d  913  orass  918  or32  922  or42  924  pm5.7  950  oranabs  996  ordir  1003  pm5.17  1008  dn1  1052  dfifp7  1064  3orrot  1088  norcom  1522  norcomOLD  1523  norass  1533  cadan  1610  cadcomb  1614  nf2  1786  nfnbi  1855  19.31v  1942  19.31  2236  r19.30OLD  3341  eueq2  3703  uncom  4131  undif3  4267  reuun2  4288  dfif2  4471  reuprg  4641  rabrsn  4662  tppreqb  4740  ssunsn2  4762  disjor  5048  zfpair  5324  somin1  5995  ordtri2  6228  on0eqel  6310  fununi  6431  eliman0  6707  swoer  8321  supgtoreq  8936  cantnflem1d  9153  cantnflem1  9154  cflim2  9687  dffin7-2  9822  fpwwe2lem13  10066  suplem2pr  10477  leloe  10729  mulcan2g  11296  fimaxre  11586  fimaxreOLD  11587  fiminre  11590  arch  11897  elznn0nn  11998  elznn0  11999  nneo  12069  ltxr  12513  xrleloe  12540  xrrebnd  12564  xmullem2  12661  xmulcom  12662  xmulneg1  12665  xmulf  12668  sqeqori  13579  hashtpg  13846  odd2np1lem  15691  lcmcom  15939  dvdsprime  16033  coprm  16057  lvecvscan2  19886  opprdomn  20076  mplcoe1  20248  mplcoe5  20251  madutpos  21253  restntr  21792  alexsubALTlem2  22658  alexsubALTlem3  22659  xrsxmet  23419  dyaddisj  24199  mdegleb  24660  atandm3  25458  wilthlem2  25648  lgsdir2lem4  25906  tgcolg  26342  hlcomb  26391  axcontlem7  26758  elntg2  26773  nb3grprlem2  27165  vtxd0nedgb  27272  clwwlkneq0  27809  eupth2lem2  28000  eupth2lem3lem6  28014  numclwwlk3lem2lem  28164  hvmulcan2  28852  elat2  30119  chrelat2i  30144  atoml2i  30162  or3dir  30228  rmounid  30261  disjnf  30322  disjorf  30331  disjex  30344  disjexc  30345  disjunsn  30346  funcnv5mpt  30415  elicoelioo  30503  xrdifh  30505  dvdszzq  30533  tlt3  30654  orngsqr  30879  ballotlemfc0  31752  ballotlemfcc  31753  bnj563  32016  subfacp1lem6  32434  3orel2  32943  dfon2lem5  33034  noextenddif  33177  sleloe  33235  btwnconn1lem14  33563  outsideofcom  33591  outsideofeu  33594  lineunray  33610  ecase13d  33663  elicc3  33667  nn0prpw  33673  bj-dfbi5  33909  bj-consensusALT  33914  topdifinfeq  34633  onsucuni3  34650  wl-cases2-dnf  34754  itg2addnclem2  34946  itgaddnclem2  34953  orfa  35362  notornotel2  35376  tsbi4  35416  ineleq  35610  leatb  36430  leat2  36432  isat3  36445  hlrelat2  36541  elpadd0  36947  ifporcor  39834  ifpim2  39844  ifpim23g  39868  ifpim123g  39873  rp-fakeoranass  39887  ontric3g  39895  elprn2  41922  stoweidlem26  42318  2reu3  43316  itschlc0xyqsol1  44760  itschlc0xyqsol  44761  inlinecirc02plem  44780