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:  equid  1681  eqvinc  2980  elnn  4769  intasym  5161  relcoi1  5304  funres11  5425  cnvresid  5427  fparlem1  6346  fparlem2  6347  dftpos4  6395  tposf12  6401  tfr2b  6554  tz7.44lem1  6560  xpcomco  7095  sbthlem2  7115  fidomdm  7285  marypha1lem  7333  hartogslem1  7404  brwdom2  7434  inf3lem6  7481  omex  7491  cantnfdm  7512  cantnfval  7516  cantnff  7522  cnfcom  7550  cnfcom2  7552  cnfcom3lem  7553  cnfcom3  7554  tz9.1c  7559  r1tr  7595  r1ord3g  7598  rankwflemb  7612  r1elwf  7615  r1elss  7625  rankval3b  7645  onssr1  7650  infxpenlem  7788  alephnbtwn  7845  alephordilem1  7847  alephfp  7882  dfac13  7915  pwsdompw  7977  infcdaabs  7979  ackbij1  8011  ackbij2  8016  r1om  8017  cflim2  8036  fin23lem27  8101  fin23lem29  8114  fin23lem30  8115  fin1a2lem6  8178  fin1a2lem7  8179  fin1a2lem13  8185  itunitc1  8193  itunitc  8194  ituniiun  8195  hsmexlem5  8203  axcc2lem  8209  axcc3  8211  zorn2lem6  8275  zorn2lem7  8276  ttukeylem6  8288  axdc  8295  fodom  8296  iunfo  8308  cardval  8315  cardid  8316  pwcfsdom  8352  alephom  8354  fpwwe  8415  canthp1lem2  8422  canthp1  8423  gchaleph2  8445  r1limwun  8505  inaprc  8605  nqerf  8701  recmulnq  8735  dmrecnq  8739  halfnq  8747  genpdm  8773  reclem3pr  8820  axresscn  8917  axpre-sup  8938  1re  8984  0re  8985  00id  9134  addid1  9139  renegcli  9255  zexALT  10193  uzn0  10394  dfle2  10633  xrinfmss  10781  axdc4uzlem  11208  facnn  11455  fac0  11456  hashgval  11508  hashinf  11510  hashrabrsn  11535  hashp1i  11559  hashxplem  11583  brfi1uzind  11602  cats1fv  11710  cnrecnv  11857  rexanuz  12036  climdm  12235  lo1eq  12249  rlimeq  12250  sumsn  12421  tanval  12616  rpnnen2lem11  12711  rpnnen  12713  sadadd2lem  12858  sadadd3  12860  sadaddlem  12865  sadasslem  12869  sadeq  12871  3prm  12983  unbenlem  13163  prmreclem6  13176  vdwlem8  13243  vdwnnlem1  13250  0ram  13275  structcnvcnv  13367  prdsval  13565  prdsbas  13567  prdsplusg  13568  prdsmulr  13569  prdsvsca  13570  prdshom  13576  xpsfrn  13681  xpsff1o2  13683  catcoppccl  14150  catcfuccl  14151  catcxpccl  14191  tsrss  14542  symgid  14991  efgmnvl  15233  efgval  15236  efgi0  15239  efgi1  15240  efgredeu  15271  0frgp  15298  lt6abl  15391  gsumval3  15401  gsumzres  15404  gsumzadd  15414  gsum2d  15433  dprdfadd  15465  dprdres  15473  dmdprdsplit2lem  15490  isdrng2  15732  drngmcl  15735  drngid2  15738  psrplusg  16336  coe1sfi  16503  ply1plusgfvi  16530  cnfldplusf  16618  cnfldsub  16619  cnsubmlem  16636  cnmsubglem  16651  gzrngunitlem  16653  mulgghm2  16676  zzngim  16723  pjfval  16823  pjpm  16825  indistpsALT  16967  tgrest  17107  leordtval2  17159  lmbr2  17206  cnprest  17234  lmff  17246  kgenidm  17459  tx1cn  17520  tx2cn  17521  hausdiag  17556  tsmsres  18039  xmetge0  18122  qdensere  18492  cnblcld  18497  cnfldms  18498  cnfldtopn  18504  xrsdsre  18529  xrge0tsms  18553  iccpnfcnv  18657  xrhmeo  18659  cnheiborlem  18667  lmmbr2  18900  lmcau  18953  cmetss  18955  cncms  18989  ovolctb  19064  ovoliunnul  19081  ismbl  19100  volf  19103  voliunlem1  19122  ioorf  19143  ioorinv  19146  ioorcl  19147  dyaddisj  19166  dyadmax  19168  dyadmbl  19170  mbfid  19206  ismbfd  19210  mbfimaopnlem  19225  limcresi  19450  dvreslem  19474  dvres2lem  19475  dvcjbr  19513  dvferm1  19547  dvferm2  19549  dvlip2  19557  dv11cn  19563  tdeglem4  19661  deg1ldg  19693  deg1leb  19696  plycpn  19884  vieta1lem2  19906  elqaa  19917  aalioulem2  19928  aaliou3lem3  19939  aaliou3lem4  19941  pserulm  20016  psercnlem2  20018  psercnlem1  20019  psercn  20020  abelth  20035  reeff1o  20041  pilem1  20045  efhalfpi  20057  coseq0negpitopi  20089  pige3  20103  efif1olem3  20124  efif1olem4  20125  efifo  20127  eff1olem  20128  logrn  20134  ellogrn  20135  relogf1o  20142  argregt0  20183  argrege0  20184  dvrelog  20206  dvloglem  20217  logf1o2  20219  dvlog  20220  efopnlem1  20225  efopnlem2  20226  logtayl  20229  cxpcn3lem  20309  cxpcn3  20310  resqrcn  20311  asinneg  20404  asinrebnd  20419  atan0  20426  atanbnd  20444  areambl  20475  sqrlim  20489  amgmlem  20506  basellem1  20541  basellem4  20544  sqff1o  20643  dchrplusg  20709  bposlem6  20751  bposlem8  20753  lgseisenlem4  20814  dchrvmasumlem2  20870  dchrisum0flblem1  20880  mulog2sum  20909  pntibndlem1  20961  pntlemo  20979  qrng0  20993  ostth  21011  vdegp1ai  21217  grporn  21311  issubgoi  21409  gidsn  21447  ginvsn  21448  rngomndo  21520  ip0i  21837  ubthlem1  21883  ubthlem2  21884  axhcompl-zf  22012  normlem7  22129  bcseqi  22133  bcsiALT  22192  hlimf  22251  hlimuni  22252  hhshsslem1  22278  hhsssh  22280  hhsscms  22290  occllem  22316  occl  22317  h1deoi  22562  h1dei  22563  h1de2ctlem  22568  h1de2ci  22569  spansni  22570  spanunsni  22592  pjpythi  22735  nmopadjlem  23103  adjcoi  23114  nmopcoadji  23115  pjoccoi  23192  shatomistici  23375  ceqsexv2d  23501  imadifxp  23561  xppreima  23582  1stpreima  23619  2ndpreima  23620  dmct  23630  xrge0neqmnf  23724  gsumpropd2lem  23732  xrge0tsmsd  23735  zzs0  23753  re0g  23758  iistmd  23776  xpinpreima  23780  xpinpreima2  23781  tpr2rico  23786  mndpluscn  23788  xrge0pluscn  23802  elrnust  23848  ustbas  23851  ustuqtop0  23864  utopsnneiplem  23871  fmucnd  23906  cnfldcusp  23937  zrhre  23972  qqhre  23973  indf1ofs  24009  brsiga  24123  cntnevol  24166  1stmbfm  24194  2ndmbfm  24195  br2base  24203  dya2iocucvr  24218  sxbrsiga  24224  dstrvprob  24298  coinflipspace  24307  coinfliprv  24309  coinflippv  24310  ballotlem1  24313  lgamucov  24391  iccllyscon  24505  rellyscon  24506  dfrdg2  24978  omsinds  25045  trpredlem1  25056  trpredtr  25059  trpredmintr  25060  wfrlem14  25095  dfrdg4  25315  elhf  25631  limsucncmpi  25711  ovoliunnfl  25756  voliunnfl  25758  areacirc  25791  filnetlem3  25921  fdc  26047  ismrer1  26153  reheibor  26154  2rexfrabdioph  26468  3rexfrabdioph  26469  4rexfrabdioph  26470  6rexfrabdioph  26471  7rexfrabdioph  26472  rencldnfi  26495  jm2.27dlem2  26694  wepwso  26730  dfac11  26751  pwssplit4  26782  frlmpwfi  26853  isnumbasgrplem3  26861  mpaaeu  26946  mvdco  26979  proot1mul  27106  proot1hash  27110  seff  27129  sumsnd  27288  stoweidlem34  27374  stoweidlem37  27377  bi123imp0  27996  tendo0co2  31036  erng1r  31243  dvalveclem  31274  dva0g  31276  dvh0g  31360
This theorem was proved from axioms:  ax-mp 8
  Copyright terms: Public domain W3C validator