MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orcom Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 pm1.4 865 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 pm1.4 865 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 210 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  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 208  df-or 844
This theorem is referenced by:  orcomd  867  unitresl  868  orbi1i  909  orbi1d  912  orass  917  or32  921  or42  923  pm5.7  949  oranabs  995  ordir  1002  pm5.17  1007  dn1  1051  dfifp7  1063  3orrot  1086  norcom  1516  norass  1526  cadan  1603  cadcomb  1607  nf2  1779  nfnbi  1848  19.31v  1935  19.31  2229  r19.30OLD  3343  eueq2  3704  uncom  4132  undif3  4268  reuun2  4289  dfif2  4471  reuprg  4637  rabrsn  4658  tppreqb  4736  ssunsn2  4758  disjor  5042  zfpair  5317  somin1  5990  ordtri2  6223  on0eqel  6305  fununi  6425  eliman0  6701  swoer  8312  supgtoreq  8926  cantnflem1d  9143  cantnflem1  9144  cflim2  9677  dffin7-2  9812  fpwwe2lem13  10056  suplem2pr  10467  leloe  10719  mulcan2g  11286  fimaxre  11576  fimaxreOLD  11577  fiminre  11580  arch  11886  elznn0nn  11987  elznn0  11988  nneo  12058  ltxr  12503  xrleloe  12530  xrrebnd  12554  xmullem2  12651  xmulcom  12652  xmulneg1  12655  xmulf  12658  sqeqori  13569  hashtpg  13836  odd2np1lem  15681  lcmcom  15929  dvdsprime  16023  coprm  16047  lvecvscan2  19806  opprdomn  19995  mplcoe1  20166  mplcoe5  20169  madutpos  21169  restntr  21708  alexsubALTlem2  22574  alexsubALTlem3  22575  xrsxmet  23334  dyaddisj  24114  mdegleb  24575  atandm3  25371  wilthlem2  25562  lgsdir2lem4  25820  tgcolg  26256  hlcomb  26305  axcontlem7  26672  elntg2  26687  nb3grprlem2  27079  vtxd0nedgb  27186  clwwlkneq0  27723  eupth2lem2  27914  eupth2lem3lem6  27928  numclwwlk3lem2lem  28078  hvmulcan2  28766  elat2  30033  chrelat2i  30058  atoml2i  30076  or3dir  30142  rmounid  30175  disjnf  30237  disjorf  30246  disjex  30259  disjexc  30260  disjunsn  30261  funcnv5mpt  30330  elicoelioo  30416  xrdifh  30418  dvdszzq  30446  tlt3  30568  orngsqr  30793  ballotlemfc0  31638  ballotlemfcc  31639  bnj563  31902  subfacp1lem6  32318  3orel2  32827  dfon2lem5  32918  noextenddif  33061  sleloe  33119  btwnconn1lem14  33447  outsideofcom  33475  outsideofeu  33478  lineunray  33494  ecase13d  33547  elicc3  33551  nn0prpw  33557  bj-dfbi5  33793  bj-consensusALT  33798  topdifinfeq  34502  onsucuni3  34519  wl-cases2-dnf  34623  itg2addnclem2  34813  itgaddnclem2  34820  orfa  35230  notornotel2  35244  tsbi4  35284  ineleq  35478  leatb  36297  leat2  36299  isat3  36312  hlrelat2  36408  elpadd0  36814  ifporcor  39694  ifpim2  39704  ifpim23g  39728  ifpim123g  39733  rp-fakeoranass  39747  ontric3g  39755  elprn2  41782  stoweidlem26  42179  2reu3  43177  itschlc0xyqsol1  44587  itschlc0xyqsol  44588  inlinecirc02plem  44607
  Copyright terms: Public domain W3C validator