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

Theorem orcom 376
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
Assertion
Ref Expression
orcom  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 375 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 375 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 180 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357
This theorem is referenced by:  orcomd  377  orbi1i  506  orass  510  or32  513  or42  515  orbi1d  683  pm5.61  693  oranabs  829  ordir  835  pm5.17  858  pm5.7  900  pm5.75  903  dn1  932  3orrot  940  3orcomb  944  cadan  1382  nf4  1800  19.31  1812  r19.30  2685  eueq2  2939  uncom  3319  reuun2  3451  dfif2  3567  ssunsn2  3773  prel12  3789  disjor  4007  zfpair  4212  ordtri2  4427  on0eqel  4510  somin1  5079  fununi  5316  swoer  6688  cantnflem1d  7390  cantnflem1  7391  cflim2  7889  dffin7-2  8024  fpwwe2lem13  8264  suplem2pr  8677  leloe  8908  fimaxre  9701  arch  9962  elznn0nn  10037  elznn0  10038  nneo  10095  ltxr  10457  xrleloe  10478  xrrebnd  10497  xmullem2  10585  xmulcom  10586  xmulneg1  10589  xmulf  10592  sqeqori  11215  odd2np1lem  12586  dvdsprime  12771  coprm  12779  lvecvscan2  15865  opprdomn  16042  mplcoe1  16209  mplcoe2  16211  restntr  16912  alexsubALTlem2  17742  alexsubALTlem3  17743  xrsxmet  18315  dyaddisj  18951  mdegleb  19450  atandm3  20174  wilthlem2  20307  lgsdir2lem4  20565  hvmulcan2  21652  elat2  22920  chrelat2i  22945  atoml2i  22963  ballotlemfc0  23051  ballotlemfcc  23052  or3dir  23124  disjex  23176  disjexc  23177  funcnv5mpt  23236  elicoelioo  23271  xrdifh  23273  disjorf  23356  subfacp1lem6  23716  eupath2lem2  23902  eupath2lem3  23903  3orel2  24062  mulcan2g  24085  dfon2lem5  24143  axcontlem7  24598  btwnconn1lem14  24723  outsideofcom  24751  outsideofeu  24754  lineunray  24770  vtarsuelt  25895  ecase13d  26222  elicc3  26228  nn0prpw  26239  stoweidlem26  27775  2reu3  27966  bnj563  28772  a12peros  29121  leatb  29482  leat2  29484  isat3  29497  hlrelat2  29592  elpadd0  29998
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator