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

Theorem orcom 394
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 393 . 2  |-  ( (
ph  \/  ps )  ->  ( ps  \/  ph ) )
2 pm1.4 393 . 2  |-  ( ( ps  \/  ph )  ->  ( ph  \/  ps ) )
31, 2impbii 192 1  |-  ( (
ph  \/  ps )  <->  ( ps  \/  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    \/ wo 375
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 190  df-or 377
This theorem is referenced by:  orcomd  395  orbi1i  529  orass  533  or32  536  or42  538  orbi1d  717  pm5.61  727  oranabs  874  ordir  882  pm5.17  905  pm5.7  948  pm5.75OLD  952  dn1  977  dfifp7  990  3orrot  1013  3orcomb  1017  cadan  1520  cadcomb  1524  stoic1aOLD  1664  19.31v  1798  nf4  2062  19.31  2067  r19.30  2921  eueq2  3200  uncom  3569  reuun2  3717  dfif2  3874  rabrsn  4033  tppreqb  4104  ssunsn2  4123  prel12  4143  disjor  4380  zfpair  4637  somin1  5239  ordtri2  5465  on0eqel  5547  fununi  5659  eliman0  5908  swoer  7409  supgtoreq  8004  cantnflem1d  8211  cantnflem1  8212  cflim2  8711  dffin7-2  8846  fpwwe2lem13  9085  suplem2pr  9496  leloe  9738  mulcan2g  10288  fimaxre  10573  arch  10890  elznn0nn  10975  elznn0  10976  nneo  11042  ltxr  11438  xrleloe  11466  xrrebnd  11486  xmullem2  11576  xmulcom  11577  xmulneg1  11580  xmulf  11583  sqeqori  12424  hashtpg  12682  odd2np1lem  14442  lcmcom  14636  dvdsprime  14716  coprm  14736  lvecvscan2  18413  opprdomn  18602  mplcoe1  18766  mplcoe5  18769  madutpos  19744  restntr  20275  alexsubALTlem2  21141  alexsubALTlem3  21142  xrsxmet  21905  dyaddisj  22633  mdegleb  23092  atandm3  23883  wilthlem2  24073  lgsdir2lem4  24333  tgcolg  24678  hlcomb  24727  axcontlem7  25079  nb3graprlem2  25259  eupath2lem2  25785  eupath2lem3  25786  hvmulcan2  26807  elat2  28074  chrelat2i  28099  atoml2i  28117  or3dir  28183  disjnf  28258  disjorf  28266  disjex  28279  disjexc  28280  disjunsn  28281  funcnv5mpt  28347  elicoelioo  28435  xrdifh  28437  tlt3  28501  orngsqr  28641  ballotlemfc0  29398  ballotlemfcc  29399  bnj563  29625  subfacp1lem6  29980  3orel2  30415  socnv  30476  dfon2lem5  30504  btwnconn1lem14  30938  outsideofcom  30966  outsideofeu  30969  lineunray  30985  ecase13d  31040  elicc3  31044  nn0prpw  31050  bj-dfbi5  31217  bj-consensusALT  31221  bj-nf2  31256  bj-nfn  31283  topdifinfeq  31823  onsucuni3  31840  wl-cases2-dnf  31920  itg2addnclem2  32058  itgaddnclem2  32065  orfa  32379  unitresl  32382  notornotel2  32396  tsbi4  32442  leatb  32929  leat2  32931  isat3  32944  hlrelat2  33039  elpadd0  33445  ifporcor  36176  ifpim2  36186  ifpim23g  36210  ifpim123g  36215  rp-fakeoranass  36229  elprn2  37811  stoweidlem26  37998  2reu3  38754  nb3grprlem2  39619  vtxd0nedgb  39711  eupth2lem2  40131  eupth2lem3lem6  40145
  Copyright terms: Public domain W3C validator