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  192  imbi12i  333  pm3.2i  462  sbcom2  2294  sstri  3427  0disj  4388  disjx0  4390  relres  5138  cnvdif  5248  difxp  5267  funopab4  5624  fun0  5649  fvsn  6113  omsinds  6730  reltpos  6996  tpostpos  7011  tpos0  7021  oaabs2  7364  swoer  7409  xpider  7452  erinxp  7455  sbthcl  7712  php  7774  inf0  8144  unctb  8653  fin1a2lem12  8859  axcc2lem  8884  axcclem  8905  brdom3  8974  brdom5  8975  brdom4  8976  pwcfsdom  9026  smobeth  9029  fpwwe2lem8  9080  fpwwe2lem9  9081  fpwwe2lem12  9084  pwxpndom2  9108  pwcdandom  9110  gchac  9124  wunex3  9184  inar1  9218  gruina  9261  ltsopi  9331  recmulnq  9407  prcdnq  9436  ltrel  9714  lerel  9716  suprfinzcl  11073  cnexALT  11321  dfle2  11469  dflt2  11470  uzrdg0i  12211  ltwefz  12215  fzennn  12219  faclbnd4lem1  12516  hashsslei  12639  0csh0  12949  isercolllem1  13805  zsum  13861  sum0  13864  znnen  14342  qnnen  14343  rpnnen  14356  ruc  14372  nthruc  14380  nthruz  14381  phicl2  14795  pwsle  15468  xpsc0  15544  xpsc1  15545  relfull  15891  relfth  15892  gicer  17018  oppglsm  17372  efgrelexlemb  17478  isunit  17963  opsrtoslem2  18785  xrsnsgrp  19081  pjpm  19348  1stcfb  20537  2ndc1stc  20543  2ndcctbss  20547  2ndcdisj2  20549  2ndcsep  20551  hmpher  20876  met1stc  21614  re2ndc  21897  iccpnfhmeo  22051  xrhmeo  22052  xrcmp  22054  xrcon  22055  dyadmbl  22637  opnmblALT  22640  vitalilem2  22646  vitalilem3  22647  vitali  22650  mbfimaopnlem  22690  mbfsup  22699  dgrval  23261  dgrcl  23266  dgrub  23267  dgrlb  23269  aannenlem3  23365  dvrelog  23661  logcn  23671  logccv  23687  logblog  23808  ppiub  24211  lgsquadlem1  24361  lgsquadlem2  24362  dirith2  24445  usgraexmpldifpr  25206  usgraexmplef  25207  disjxwwlks  25543  disjxwwlkn  25552  konigsberg  25794  nvrel  26302  phrel  26537  bnrel  26590  hlrel  26623  pjnormi  27455  lnopunilem1  27744  lnophmlem1  27750  xrge0infssd  28417  xrge0infssdOLD  28418  infxrge0lb  28421  infxrge0lbOLD  28422  infxrge0glb  28423  infxrge0glbOLD  28424  infxrge0gelb  28425  infxrge0gelbOLD  28426  ssnnssfz  28442  xrge0iifiso  28815  omsf  29193  omsfOLD  29197  oms0  29198  omssubaddlem  29200  omssubadd  29201  oms0OLD  29202  omssubaddlemOLD  29204  omssubaddOLD  29205  oddpwdc  29260  bnj1023  29664  bnj1109  29670  erdszelem4  29989  erdszelem8  29993  supfz  30434  inffz  30435  elrn3  30474  trer  31043  fneer  31080  naim1i  31118  naim2i  31119  mont  31140  onpsstopbas  31161  bj-mp2c  31193  bj-mp2d  31194  bj-alrimih  31273  wl-equsal1i  31946  wl-sbcom2d  31961  poimirlem26  32030  mblfinlem1  32041  incsequz2  32142  cncfres  32161  heiborlem3  32209  diclspsn  34833  dih1dimatlem  34968  rencldnfilem  35734  pellexlem4  35747  pellexlem5  35748  ttac  35962  idomsubgmo  36143  areaquad  36172  frege102  36632  lhe4.4ex1a  36748  eel0001  37168  eel0000  37169  eel00001  37171  eel00000  37172  e000  37217  e00  37218  fzisoeu  37606  resincncf  37849  ssnn0ssfz  40638  zlmodzxzldeplem  40799