Theorem mp2 9

Description: A double modus ponens inference. (Contributed by NM, 5-Apr-1994.)

Hypotheses

Ref	Expression
mp2.1	|- ph
mp2.2	|- ps
mp2.3	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mp2	|- ch

Proof of Theorem mp2

Step	Hyp	Ref	Expression
1		mp2.2	. 2 |- ps
2		mp2.1	. . 3 |- ph
3		mp2.3	. . 3 |- ( ph -> ( ps -> ch ) )
4	2, 3	ax-mp 5	. 2 |- ( ps -> ch )
5	1, 4	ax-mp 5	1 |- ch

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by:  impbii  199  imbi12i  340  pm3.2i  471  minimp-sylsimp  1561  minimp-ax2c  1563  minimp-ax2  1564  minimp-pm2.43  1565  sbcom2  2445  sstri  3612  0disj  4645  disjx0  4647  relres  5426  cnvdif  5539  difxp  5558  funopab4  5925  fun0  5954  fvsn  6446  omsinds  7084  reltpos  7357  tpostpos  7372  tpos0  7382  oaabs2  7725  swoer  7772  xpider  7818  erinxp  7821  sbthcl  8082  php  8144  elirrv  8504  inf0  8518  unctb  9027  fin1a2lem12  9233  axcc2lem  9258  axcclem  9279  brdom3  9350  brdom5  9351  brdom4  9352  pwcfsdom  9405  smobeth  9408  fpwwe2lem8  9459  fpwwe2lem9  9460  fpwwe2lem12  9463  pwxpndom2  9487  pwcdandom  9489  gchac  9503  wunex3  9563  inar1  9597  gruina  9640  ltsopi  9710  recmulnq  9786  prcdnq  9815  ltrel  10100  lerel  10102  suprfinzcl  11492  cnexALT  11828  dfle2  11980  dflt2  11981  uzrdg0i  12758  ltwefz  12762  fzennn  12767  faclbnd4lem1  13080  hashsslei  13213  0csh0  13539  isercolllem1  14395  zsum  14449  sum0  14452  znnen  14941  qnnen  14942  rpnnen  14956  ruc  14972  nthruc  14981  nthruz  14982  phicl2  15473  pwsle  16152  xpsc0  16220  xpsc1  16221  relfull  16568  relfth  16569  gicer  17718  gicerOLD  17719  oppglsm  18057  efgrelexlemb  18163  isunit  18657  opsrtoslem2  19485  xrsnsgrp  19782  pjpm  20052  1stcfb  21248  2ndc1stc  21254  2ndcctbss  21258  2ndcdisj2  21260  2ndcsep  21262  hmpher  21587  met1stc  22326  re2ndc  22604  iccpnfhmeo  22744  xrhmeo  22745  xrcmp  22747  xrconn  22748  dyadmbl  23368  opnmblALT  23371  vitalilem2  23378  vitalilem3  23379  vitali  23382  mbfimaopnlem  23422  mbfsup  23431  dgrval  23984  dgrcl  23989  dgrub  23990  dgrlb  23992  aannenlem3  24085  dvrelog  24383  logcn  24393  logccv  24409  logblog  24530  ppiub  24929  lgsquadlem1  25105  lgsquadlem2  25106  dirith2  25217  usgrexmpldifpr  26150  usgrexmplef  26151  disjxwwlksn  26799  disjxwwlkn  26808  nvrel  27457  phrel  27670  bnrel  27723  hlrel  27746  pjnormi  28580  lnopunilem1  28869  lnophmlem1  28875  xrge0infssd  29526  infxrge0lb  29529  infxrge0glb  29530  infxrge0gelb  29531  ssnnssfz  29549  xrge0iifiso  29981  omsf  30358  oms0  30359  omssubaddlem  30361  omssubadd  30362  oddpwdc  30416  rpsqrtcn  30671  bnj1023  30851  bnj1109  30857  erdszelem4  31176  erdszelem8  31180  supfz  31613  inffz  31614  inffzOLD  31615  elrn3  31652  trer  32310  fneer  32348  naim1i  32386  naim2i  32387  mont  32408  onpsstopbas  32429  bj-mp2c  32531  bj-mp2d  32532  bj-currypeirce  32544  wl-equsal1i  33329  wl-sbcom2d  33344  poimirlem25  33434  poimirlem26  33435  mblfinlem1  33446  incsequz2  33545  cncfres  33564  heiborlem3  33612  diclspsn  36483  dih1dimatlem  36618  rencldnfilem  37384  pellexlem4  37396  pellexlem5  37397  ttac  37603  idomsubgmo  37776  areaquad  37802  frege102  38259  lhe4.4ex1a  38528  eel0001  38945  eel0000  38946  eel00001  38948  eel00000  38949  e000  38994  e00  38995  fzisoeu  39514  resincncf  40088  fmtnoinf  41448  ssnn0ssfz  42127  zlmodzxzldeplem  42287