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  1812  19.31  1824  r19.30  2698  eueq2  2952  uncom  3332  reuun2  3464  dfif2  3580  ssunsn2  3789  prel12  3805  disjor  4023  zfpair  4228  ordtri2  4443  on0eqel  4526  somin1  5095  fununi  5332  swoer  6704  cantnflem1d  7406  cantnflem1  7407  cflim2  7905  dffin7-2  8040  fpwwe2lem13  8280  suplem2pr  8693  leloe  8924  fimaxre  9717  arch  9978  elznn0nn  10053  elznn0  10054  nneo  10111  ltxr  10473  xrleloe  10494  xrrebnd  10513  xmullem2  10601  xmulcom  10602  xmulneg1  10605  xmulf  10608  sqeqori  11231  odd2np1lem  12602  dvdsprime  12787  coprm  12795  lvecvscan2  15881  opprdomn  16058  mplcoe1  16225  mplcoe2  16227  restntr  16928  alexsubALTlem2  17758  alexsubALTlem3  17759  xrsxmet  18331  dyaddisj  18967  mdegleb  19466  atandm3  20190  wilthlem2  20323  lgsdir2lem4  20581  hvmulcan2  21668  elat2  22936  chrelat2i  22961  atoml2i  22979  ballotlemfc0  23067  ballotlemfcc  23068  or3dir  23140  disjex  23192  disjexc  23193  funcnv5mpt  23251  elicoelioo  23286  xrdifh  23288  disjorf  23371  subfacp1lem6  23731  eupath2lem2  23917  eupath2lem3  23918  3orel2  24077  mulcan2g  24100  dfon2lem5  24214  axcontlem7  24670  btwnconn1lem14  24795  outsideofcom  24823  outsideofeu  24826  lineunray  24842  itg2addnclem2  25004  vtarsuelt  25998  ecase13d  26325  elicc3  26331  nn0prpw  26342  stoweidlem26  27878  2reu3  28069  hashtpg  28217  nb3graprlem2  28288  bnj563  29088  a12peros  29743  leatb  30104  leat2  30106  isat3  30119  hlrelat2  30214  elpadd0  30620
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