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  2647  eueq2  2876  uncom  3229  reuun2  3358  dfif2  3472  ssunsn2  3673  prel12  3689  disjor  3904  zfpair  4106  ordtri2  4320  on0eqel  4401  somin1  4986  fununi  5173  swoer  6574  cantnflem1d  7274  cantnflem1  7275  cflim2  7773  dffin7-2  7908  fpwwe2lem13  8144  suplem2pr  8557  leloe  8788  fimaxre  9581  arch  9841  elznn0nn  9916  elznn0  9917  nneo  9974  ltxr  10336  xrleloe  10357  xrrebnd  10376  xmullem2  10463  xmulcom  10464  xmulneg1  10467  xmulf  10470  sqeqori  11093  odd2np1lem  12460  dvdsprime  12645  coprm  12653  lvecvscan2  15700  opprdomn  15874  mplcoe1  16041  mplcoe2  16043  restntr  16744  alexsubALTlem2  17574  alexsubALTlem3  17575  xrsxmet  18147  dyaddisj  18783  mdegleb  19282  atandm3  20006  wilthlem2  20139  lgsdir2lem4  20397  hvmulcan2  21482  elat2  22750  chrelat2i  22775  atoml2i  22793  subfacp1lem6  22887  eupath2lem2  23073  eupath2lem3  23074  3orel2  23233  mulcan2g  23255  dfon2lem5  23311  axcontlem7  23772  btwnconn1lem14  23897  outsideofcom  23925  outsideofeu  23928  lineunray  23944  vtarsuelt  25061  ecase13d  25388  elicc3  25394  nn0prpw  25405  bnj563  27461  a12peros  27810  leatb  28171  leat2  28173  isat3  28186  hlrelat2  28281  elpadd0  28687
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