Theorem mp2 9

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

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  188  imbi12i  326  pm3.2i  455  sbcom2  2175  sstri  3498  0disj  4430  disjx0  4432  relres  5291  cnvdif  5402  difxp  5421  funopab4  5613  fun0  5635  fvsn  6089  reltpos  6962  tpostpos  6977  tpos0  6987  oaabs2  7296  swoer  7341  xpider  7384  erinxp  7387  sbthcl  7641  php  7703  inf0  8041  unctb  8588  fin1a2lem12  8794  axcc2lem  8819  axcclem  8840  brdom3  8909  brdom5  8910  brdom4  8911  pwcfsdom  8961  smobeth  8964  fpwwe2lem8  9018  fpwwe2lem9  9019  fpwwe2lem12  9022  pwxpndom2  9046  pwcdandom  9048  gchac  9062  wunex3  9122  inar1  9156  gruina  9199  ltsopi  9269  recmulnq  9345  prcdnq  9374  ltrel  9652  lerel  9654  suprfinzcl  10983  cnexALT  11225  dfle2  11362  dflt2  11363  uzrdg0i  12049  ltwefz  12053  fzennn  12057  faclbnd4lem1  12350  hashsslei  12463  0csh0  12743  isercolllem1  13466  zsum  13519  sum0  13522  xpnnenOLD  13820  znnen  13823  qnnen  13824  rpnnen  13837  ruc  13853  nthruc  13861  nthruz  13862  phicl2  14175  pwsle  14766  xpsc0  14834  xpsc1  14835  relfull  15151  relfth  15152  gicer  16198  oppglsm  16536  efgrelexlemb  16642  isunit  17180  opsrtoslem2  18023  xrsnsgrp  18328  pjpm  18612  1stcfb  19819  2ndc1stc  19825  2ndcctbss  19829  2ndcdisj2  19831  2ndcsep  19833  hmpher  20158  met1stc  20897  re2ndc  21179  iccpnfhmeo  21318  xrhmeo  21319  xrcmp  21321  xrcon  21322  dyadmbl  21882  opnmblALT  21885  vitalilem2  21891  vitalilem3  21892  vitali  21895  mbfimaopnlem  21935  mbfsup  21944  dgrval  22498  dgrcl  22503  dgrub  22504  dgrlb  22506  aannenlem3  22598  dvrelog  22890  logcn  22900  logccv  22916  ppiub  23351  lgsquadlem1  23501  lgsquadlem2  23502  dirith2  23585  usgraexmpldifpr  24272  usgraexmpl  24273  disjxwwlks  24608  disjxwwlkn  24617  konigsberg  24859  nvrel  25367  phrel  25602  bnrel  25655  hlrel  25678  pjnormi  26511  lnopunilem1  26801  lnophmlem1  26807  xrge0infssd  27453  ssnnssfz  27469  xrge0iifiso  27790  oms0  28139  oddpwdc  28166  erdszelem4  28511  erdszelem8  28515  supfz  28980  inffz  28981  elrn3  29167  omsinds  29274  naim1i  29827  naim2i  29828  mont  29849  onpsstopbas  29870  wl-equsal1i  29971  wl-sbcom2d  29986  mblfinlem1  30026  trer  30109  fneer  30146  incsequz2  30217  cncfres  30236  heiborlem3  30284  rencldnfilem  30729  pellexlem4  30743  pellexlem5  30744  ttac  30953  idomsubgmo  31131  areaquad  31160  lhe4.4ex1a  31210  fzisoeu  31449  resincncf  31584  ssnn0ssfz  32671  zlmodzxzldeplem  32834  eel0001  33248  eel0000  33249  eel00001  33251  eel00000  33252  e000  33297  e00  33298  bnj1023  33572  bnj1109  33578  bj-mp2c  33862  bj-mp2d  33863  bj-alrimih  33957  diclspsn  36661  dih1dimatlem  36796