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 208	1 ⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))

Syntax hints:   ↔ wb 205   ∨ 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 206  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  1055  dfifp7  1067  3orrot  1091  3orel2  1484  norcom  1527  norcomOLD  1528  norass  1535  cadan  1611  cadcomb  1615  nf2  1788  nfnbiOLD  1858  19.31v  1944  19.31  2227  2ralor  3296  eueq2  3645  uncom  4087  undif3  4224  reuun2  4248  dfif2  4461  reuprg  4639  rabrsn  4660  tppreqb  4738  ssunsn2  4760  dfopif  4800  disjor  5054  zfpair  5344  somin1  6038  ordtri2  6301  on0eqel  6384  fununi  6509  eliman0  6809  swoer  8528  supgtoreq  9229  cantnflem1d  9446  cantnflem1  9447  cflim2  10019  dffin7-2  10154  fpwwe2lem12  10398  suplem2pr  10809  leloe  11061  mulcan2g  11629  fimaxre  11919  fiminre  11922  arch  12230  elznn0nn  12333  elznn0  12334  nneo  12404  ltxr  12851  xrleloe  12878  xrrebnd  12902  xmullem2  12999  xmulcom  13000  xmulneg1  13003  xmulf  13006  sqeqori  13930  hashtpg  14199  odd2np1lem  16049  lcmcom  16298  dvdsprime  16392  coprm  16416  lvecvscan2  20374  opprdomn  20572  mplcoe1  21238  mplcoe5  21241  madutpos  21791  restntr  22333  alexsubALTlem2  23199  alexsubALTlem3  23200  xrsxmet  23972  dyaddisj  24760  mdegleb  25229  atandm3  26028  wilthlem2  26218  lgsdir2lem4  26476  tgcolg  26915  hlcomb  26964  axcontlem7  27338  elntg2  27353  nb3grprlem2  27748  vtxd0nedgb  27855  clwwlkneq0  28393  eupth2lem2  28583  eupth2lem3lem6  28597  numclwwlk3lem2lem  28747  hvmulcan2  29435  elat2  30702  chrelat2i  30727  atoml2i  30745  or3dir  30811  rmounid  30843  disjnf  30909  disjorf  30918  disjex  30931  disjexc  30932  disjunsn  30933  funcnv5mpt  31005  elicoelioo  31099  xrdifh  31101  dvdszzq  31129  tlt3  31248  orngsqr  31503  ballotlemfc0  32459  ballotlemfcc  32460  bnj563  32723  subfacp1lem6  33147  dfon2lem5  33763  poxp2  33790  noextenddif  33871  sleloe  33957  btwnconn1lem14  34402  outsideofcom  34430  outsideofeu  34433  lineunray  34449  ecase13d  34502  elicc3  34506  nn0prpw  34512  bj-dfbi5  34755  bj-consensusALT  34760  topdifinfeq  35521  onsucuni3  35538  wl-ifpimpr  35637  wl-cases2-dnf  35671  itg2addnclem2  35829  itgaddnclem2  35836  orfa  36240  notornotel2  36254  tsbi4  36294  ineleq  36486  leatb  37306  leat2  37308  isat3  37321  hlrelat2  37417  elpadd0  37823  fsuppind  40279  ifporcor  41069  ifpim2  41079  ifpim23g  41102  ifpim123g  41107  rp-fakeoranass  41121  ontric3g  41129  elprn2  43175  stoweidlem26  43567  2reu3  44602  itschlc0xyqsol1  46112  itschlc0xyqsol  46113  inlinecirc02plem  46132