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

Theorem orcom 378
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 377 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 377 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 182 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359
This theorem is referenced by:  orcomd  379  orbi1i  508  orass  512  or32  515  or42  517  orbi1d  686  pm5.61  696  oranabs  832  ordir  838  pm5.17  863  pm5.7  905  pm5.75  908  dn1  937  3orrot  945  3orcomb  949  cadan  1388  nf4  1780  19.31  1795  r19.30  2660  eueq2  2914  uncom  3294  reuun2  3426  dfif2  3541  ssunsn2  3747  prel12  3763  disjor  3981  zfpair  4184  ordtri2  4399  on0eqel  4482  somin1  5067  fununi  5254  swoer  6656  cantnflem1d  7358  cantnflem1  7359  cflim2  7857  dffin7-2  7992  fpwwe2lem13  8232  suplem2pr  8645  leloe  8876  fimaxre  9669  arch  9929  elznn0nn  10004  elznn0  10005  nneo  10062  ltxr  10424  xrleloe  10445  xrrebnd  10464  xmullem2  10551  xmulcom  10552  xmulneg1  10555  xmulf  10558  sqeqori  11181  odd2np1lem  12548  dvdsprime  12733  coprm  12741  lvecvscan2  15827  opprdomn  16004  mplcoe1  16171  mplcoe2  16173  restntr  16874  alexsubALTlem2  17704  alexsubALTlem3  17705  xrsxmet  18277  dyaddisj  18913  mdegleb  19412  atandm3  20136  wilthlem2  20269  lgsdir2lem4  20527  hvmulcan2  21612  elat2  22880  chrelat2i  22905  atoml2i  22923  ballotlemfc0  23012  ballotlemfcc  23013  subfacp1lem6  23088  eupath2lem2  23274  eupath2lem3  23275  3orel2  23434  mulcan2g  23456  dfon2lem5  23512  axcontlem7  23973  btwnconn1lem14  24098  outsideofcom  24126  outsideofeu  24129  lineunray  24145  vtarsuelt  25262  ecase13d  25589  elicc3  25595  nn0prpw  25606  stoweidlem26  27110  bnj563  27821  a12peros  28288  leatb  28649  leat2  28651  isat3  28664  hlrelat2  28759  elpadd0  29165
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator