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

Theorem orcom 385
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-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 384 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 384 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 187 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 368
This theorem is referenced by:  orcomd  386  orbi1i  518  orass  522  or32  525  or42  527  orbi1d  701  pm5.61  711  oranabs  857  ordir  866  pm5.17  889  pm5.7  935  pm5.75  938  dn1  967  3orrot  980  3orcomb  984  dfifp7  1393  cadan  1474  cadcomb  1480  stoic1aOLD  1626  19.31v  1756  nf4  1990  19.31  1996  r19.30  2952  eueq2  3223  uncom  3587  reuun2  3733  dfif2  3887  rabrsn  4042  tppreqb  4113  ssunsn2  4131  prel12  4149  disjor  4380  zfpair  4628  somin1  5221  ordtri2  5445  on0eqel  5527  fununi  5635  eliman0  5878  swoer  7376  supgtoreq  7962  cantnflem1d  8139  cantnflem1  8140  cantnflem1dOLD  8162  cantnflem1OLD  8163  cflim2  8675  dffin7-2  8810  fpwwe2lem13  9050  suplem2pr  9461  leloe  9702  mulcan2g  10244  fimaxre  10530  arch  10833  elznn0nn  10919  elznn0  10920  nneo  10987  ltxr  11377  xrleloe  11403  xrrebnd  11422  xmullem2  11510  xmulcom  11511  xmulneg1  11514  xmulf  11517  sqeqori  12324  hashtpg  12572  odd2np1lem  14254  dvdsprime  14439  coprm  14450  lvecvscan2  18078  opprdomn  18270  mplcoe1  18447  mplcoe5  18451  mplcoe2OLD  18453  madutpos  19436  restntr  19976  alexsubALTlem2  20840  alexsubALTlem3  20841  xrsxmet  21606  dyaddisj  22297  mdegleb  22756  atandm3  23534  wilthlem2  23724  lgsdir2lem4  23982  tgcolg  24324  hlcomb  24371  axcontlem7  24690  nb3graprlem2  24869  eupath2lem2  25395  eupath2lem3  25396  hvmulcan2  26404  elat2  27672  chrelat2i  27697  atoml2i  27715  or3dir  27781  disjnf  27863  disjorf  27871  disjex  27884  disjexc  27885  disjunsn  27886  funcnv5mpt  27954  elicoelioo  28037  xrdifh  28039  tlt3  28105  orngsqr  28247  ballotlemfc0  28937  ballotlemfcc  28938  bnj563  29127  subfacp1lem6  29482  3orel2  29917  socnv  29978  dfon2lem5  30006  btwnconn1lem14  30438  outsideofcom  30466  outsideofeu  30469  lineunray  30485  ecase13d  30541  elicc3  30545  nn0prpw  30551  bj-dfbi5  30721  bj-nf2  30760  bj-nfn  30783  topdifinfeq  31267  wl-cases2-dnf  31337  itg2addnclem2  31440  itgaddnclem2  31447  orfa  31761  unitresl  31764  notornotel2  31778  tsbi4  31825  leatb  32310  leat2  32312  isat3  32325  hlrelat2  32420  elpadd0  32826  ifporcor  35552  ifpim2  35562  ifpim23g  35586  ifpim123g  35591  rp-fakeoranass  35605  lcmcom  36047  elprn2  37008  stoweidlem26  37176  2reu3  37561
  Copyright terms: Public domain W3C validator