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

Theorem mp2b 9
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.)
Hypotheses
Ref Expression
mp2b.1  |-  ph
mp2b.2  |-  ( ph  ->  ps )
mp2b.3  |-  ( ps 
->  ch )
Assertion
Ref Expression
mp2b  |-  ch

Proof of Theorem mp2b
StepHypRef Expression
1 mp2b.1 . . 3  |-  ph
2 mp2b.2 . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 8 . 2  |-  ps
4 mp2b.3 . 2  |-  ( ps 
->  ch )
53, 4ax-mp 8 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  eqvinc  2895  elnn  4666  intasym  5058  relcoi1  5201  funres11  5320  cnvresid  5322  fparlem1  6218  fparlem2  6219  dftpos4  6253  tposf12  6259  tfr2b  6412  tz7.44lem1  6418  xpcomco  6952  sbthlem2  6972  fidomdm  7138  marypha1lem  7186  hartogslem1  7257  brwdom2  7287  inf3lem6  7334  omex  7344  cantnfdm  7365  cantnfval  7369  cantnff  7375  cnfcom  7403  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  tz9.1c  7412  r1tr  7448  r1ord3g  7451  rankwflemb  7465  r1elwf  7468  r1elss  7478  rankval3b  7498  onssr1  7503  infxpenlem  7641  alephnbtwn  7698  alephordilem1  7700  alephfp  7735  dfac13  7768  pwsdompw  7830  infcdaabs  7832  ackbij1  7864  ackbij2  7869  r1om  7870  cflim2  7889  fin23lem27  7954  fin23lem29  7967  fin23lem30  7968  fin1a2lem6  8031  fin1a2lem7  8032  fin1a2lem13  8038  itunitc1  8046  itunitc  8047  ituniiun  8048  hsmexlem5  8056  axcc2lem  8062  axcc3  8064  zorn2lem6  8128  zorn2lem7  8129  ttukeylem6  8141  axdc  8148  fodom  8149  iunfo  8161  cardval  8168  cardid  8169  pwcfsdom  8205  alephom  8207  fpwwe  8268  canthp1lem2  8275  canthp1  8276  gchaleph2  8298  r1limwun  8358  inaprc  8458  nqerf  8554  recmulnq  8588  dmrecnq  8592  halfnq  8600  genpdm  8626  reclem3pr  8673  axresscn  8770  axpre-sup  8791  1re  8837  0re  8838  00id  8987  addid1  8992  renegcli  9108  zexALT  10042  uzn0  10243  dfle2  10481  xrinfmss  10628  axdc4uzlem  11044  facnn  11290  fac0  11291  hashgval  11340  hashinf  11342  hashp1i  11369  hashxplem  11385  cats1fv  11509  cnrecnv  11650  rexanuz  11829  climdm  12028  lo1eq  12042  rlimeq  12043  sumsn  12213  tanval  12408  rpnnen2lem11  12503  rpnnen  12505  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  3prm  12775  unbenlem  12955  prmreclem6  12968  vdwlem8  13035  vdwnnlem1  13042  0ram  13067  structcnvcnv  13159  prdsval  13355  prdsbas  13357  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  prdshom  13366  xpsfrn  13471  xpsff1o2  13473  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981  tsrss  14332  symgid  14781  efgmnvl  15023  efgval  15026  efgi0  15029  efgi1  15030  efgredeu  15061  0frgp  15088  lt6abl  15181  gsumval3  15191  gsumzres  15194  gsumzadd  15204  gsum2d  15223  dprdfadd  15255  dprdres  15263  dmdprdsplit2lem  15280  isdrng2  15522  drngmcl  15525  drngid2  15528  psrplusg  16126  coe1sfi  16293  ply1plusgfvi  16320  cnfldplusf  16401  cnfldsub  16402  cnsubmlem  16419  cnmsubglem  16434  gzrngunitlem  16436  mulgghm2  16459  zzngim  16506  pjfval  16606  pjpm  16608  indistpsALT  16750  tgrest  16890  leordtval2  16942  lmbr2  16989  cnprest  17017  lmff  17029  kgenidm  17242  tx1cn  17303  tx2cn  17304  hausdiag  17339  tsmsres  17826  xmetge0  17909  qdensere  18279  cnblcld  18284  cnfldms  18285  cnfldtopn  18291  xrsdsre  18316  xrge0tsms  18339  iccpnfcnv  18442  xrhmeo  18444  cnheiborlem  18452  lmmbr2  18685  lmcau  18738  cmetss  18740  cncms  18774  ovolctb  18849  ovoliunnul  18866  ismbl  18885  volf  18888  voliunlem1  18907  ioorf  18928  ioorinv  18931  ioorcl  18932  dyaddisj  18951  dyadmax  18953  dyadmbl  18955  mbfid  18991  ismbfd  18995  mbfimaopnlem  19010  limcresi  19235  dvreslem  19259  dvres2lem  19260  dvcjbr  19298  dvferm1  19332  dvferm2  19334  dvlip2  19342  dv11cn  19348  tdeglem4  19446  deg1ldg  19478  deg1leb  19481  plycpn  19669  vieta1lem2  19691  elqaa  19702  aalioulem2  19713  aaliou3lem3  19724  aaliou3lem4  19726  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  abelth  19817  reeff1o  19823  pilem1  19827  efhalfpi  19839  coseq0negpitopi  19871  pige3  19885  efif1olem3  19906  efif1olem4  19907  efifo  19909  eff1olem  19910  logrn  19916  ellogrn  19917  relogf1o  19924  argregt0  19964  argrege0  19965  dvrelog  19984  dvloglem  19995  logf1o2  19997  dvlog  19998  efopnlem1  20003  efopnlem2  20004  logtayl  20007  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  asinneg  20182  asinrebnd  20197  atan0  20204  atanbnd  20222  areambl  20253  sqrlim  20267  amgmlem  20284  basellem1  20318  basellem4  20321  sqff1o  20420  dchrplusg  20486  bposlem6  20528  bposlem8  20530  lgseisenlem4  20591  dchrvmasumlem2  20647  dchrisum0flblem1  20657  mulog2sum  20686  pntibndlem1  20738  pntlemo  20756  qrng0  20770  ostth  20788  grporn  20879  issubgoi  20977  gidsn  21015  ginvsn  21016  rngomndo  21088  ip0i  21403  ubthlem1  21449  ubthlem2  21450  axhcompl-zf  21578  normlem7  21695  bcseqi  21699  bcsiALT  21758  hlimf  21817  hlimuni  21818  hhshsslem1  21844  hhsssh  21846  hhsscms  21856  occllem  21882  occl  21883  h1deoi  22128  h1dei  22129  h1de2ctlem  22134  h1de2ci  22135  spansni  22136  spanunsni  22158  pjpythi  22301  nmopadjlem  22669  adjcoi  22680  nmopcoadji  22681  pjoccoi  22758  shatomistici  22941  ballotlem1  23045  ceqsexv2d  23162  cntnevol  23175  xppreima  23211  iistmd  23286  xpinpreima  23290  xpinpreima2  23291  tpr2rico  23296  mndpluscn  23299  xrge0pluscn  23322  xrge0neqmnf  23330  dmct  23342  gsumpropd2lem  23379  xrge0tsmsd  23382  brsiga  23514  1stmbfm  23565  2ndmbfm  23566  br2base  23574  indf1ofs  23609  dstrvprob  23672  coinflipspace  23681  coinfliprv  23683  coinflippv  23684  iccllyscon  23781  rellyscon  23782  vdegp1ai  23908  dfrdg2  24152  omsinds  24219  trpredlem1  24230  trpredtr  24233  trpredmintr  24234  wfrlem14  24269  dfrdg4  24488  elhf  24804  limsucncmpi  24884  areacirc  24931  scprefat  25071  scprefat2  25072  domrancur1c  25202  bsi  25501  limptlimpr2lem2  25575  dtt1  25588  intrn  25599  bsi2  25639  bsi3  25641  bsi4  25643  addcanri  25666  issrc  25867  tartarmap  25888  prismorcsetlemc  25917  idcatfun  25941  lemindclsbu  25995  pgapspf  26052  pdiveql  26168  filnetlem3  26329  fdc  26455  ismrer1  26562  reheibor  26563  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  rencldnfi  26904  jm2.27dlem2  27103  wepwso  27139  dfac11  27160  pwssplit4  27191  frlmpwfi  27262  isnumbasgrplem3  27270  mpaaeu  27355  mvdco  27388  proot1mul  27515  proot1hash  27519  seff  27538  sumsnd  27697  stoweidlem34  27783  stoweidlem37  27786  tendo0co2  30977  erng1r  31184  dvalveclem  31215  dva0g  31217  dvh0g  31301
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator