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  685  pm5.61  695  oranabs  831  ordir  837  pm5.17  860  pm5.7  902  pm5.75  905  dn1  934  3orrot  942  3orcomb  946  cadan  1384  nf4  1802  19.31  1814  r19.30  2687  eueq2  2941  uncom  3321  reuun2  3453  dfif2  3569  ssunsn2  3775  prel12  3791  disjor  4009  zfpair  4212  ordtri2  4427  on0eqel  4510  somin1  5079  fununi  5282  swoer  6684  cantnflem1d  7386  cantnflem1  7387  cflim2  7885  dffin7-2  8020  fpwwe2lem13  8260  suplem2pr  8673  leloe  8904  fimaxre  9697  arch  9958  elznn0nn  10033  elznn0  10034  nneo  10091  ltxr  10453  xrleloe  10474  xrrebnd  10493  xmullem2  10580  xmulcom  10581  xmulneg1  10584  xmulf  10587  sqeqori  11210  odd2np1lem  12581  dvdsprime  12766  coprm  12774  lvecvscan2  15860  opprdomn  16037  mplcoe1  16204  mplcoe2  16206  restntr  16907  alexsubALTlem2  17737  alexsubALTlem3  17738  xrsxmet  18310  dyaddisj  18946  mdegleb  19445  atandm3  20169  wilthlem2  20302  lgsdir2lem4  20560  hvmulcan2  21645  elat2  22913  chrelat2i  22938  atoml2i  22956  ballotlemfc0  23045  ballotlemfcc  23046  subfacp1lem6  23121  eupath2lem2  23307  eupath2lem3  23308  3orel2  23467  mulcan2g  23489  dfon2lem5  23545  axcontlem7  24006  btwnconn1lem14  24131  outsideofcom  24159  outsideofeu  24162  lineunray  24178  vtarsuelt  25295  ecase13d  25622  elicc3  25628  nn0prpw  25639  stoweidlem26  27175  2reu3  27346  bnj563  28040  a12peros  28389  leatb  28750  leat2  28752  isat3  28765  hlrelat2  28860  elpadd0  29266
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