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  2173  sstri  3513  0disj  4440  disjx0  4442  relres  5299  cnvdif  5410  difxp  5429  funopab4  5621  fun0  5643  fvsn  6092  reltpos  6957  tpostpos  6972  tpos0  6982  oaabs2  7291  swoer  7336  xpider  7379  erinxp  7382  sbthcl  7636  php  7698  inf0  8034  unctb  8581  fin1a2lem12  8787  axcc2lem  8812  axcclem  8833  brdom3  8902  brdom5  8903  brdom4  8904  pwcfsdom  8954  smobeth  8957  fpwwe2lem8  9011  fpwwe2lem9  9012  fpwwe2lem12  9015  pwxpndom2  9039  pwcdandom  9041  gchac  9055  wunex3  9115  inar1  9149  gruina  9192  ltsopi  9262  recmulnq  9338  prcdnq  9367  ltrel  9645  lerel  9647  suprfinzcl  10971  cnexALT  11212  dfle2  11349  dflt2  11350  uzrdg0i  12034  ltwefz  12038  fzennn  12042  faclbnd4lem1  12335  hashsslei  12445  0csh0  12723  isercolllem1  13446  zsum  13499  sum0  13502  xpnnenOLD  13800  znnen  13803  qnnen  13804  rpnnen  13817  ruc  13833  nthruc  13841  nthruz  13842  phicl2  14153  pwsle  14743  xpsc0  14811  xpsc1  14812  relfull  15131  relfth  15132  gicer  16119  oppglsm  16458  efgrelexlemb  16564  isunit  17090  opsrtoslem2  17920  pjpm  18506  1stcfb  19712  2ndc1stc  19718  2ndcctbss  19722  2ndcdisj2  19724  2ndcsep  19726  hmpher  20020  met1stc  20759  re2ndc  21041  iccpnfhmeo  21180  xrhmeo  21181  xrcmp  21183  xrcon  21184  dyadmbl  21744  opnmblALT  21747  vitalilem2  21753  vitalilem3  21754  vitali  21757  mbfimaopnlem  21797  mbfsup  21806  dgrval  22360  dgrcl  22365  dgrub  22366  dgrlb  22368  aannenlem3  22460  dvrelog  22746  logcn  22756  logccv  22772  ppiub  23207  lgsquadlem1  23357  lgsquadlem2  23358  dirith2  23441  usgraexmpldifpr  24076  usgraexmpl  24077  disjxwwlks  24412  disjxwwlkn  24421  konigsberg  24663  nvrel  25171  phrel  25406  bnrel  25459  hlrel  25482  pjnormi  26315  lnopunilem1  26605  lnophmlem1  26611  xrge0infssd  27249  ssnnssfz  27265  xrge0iifiso  27553  oms0  27906  oddpwdc  27933  erdszelem4  28278  erdszelem8  28282  supfz  28582  inffz  28583  elrn3  28769  omsinds  28876  naim1i  29429  naim2i  29430  mont  29451  onpsstopbas  29472  wl-equsal1i  29573  wl-sbcom2d  29588  mblfinlem1  29628  trer  29711  fneer  29760  incsequz2  29845  cncfres  29864  heiborlem3  29912  rencldnfilem  30358  pellexlem4  30372  pellexlem5  30373  ttac  30582  idomsubgmo  30760  areaquad  30789  lhe4.4ex1a  30834  fzisoeu  31077  resincncf  31213  ssnn0ssfz  32002  zlmodzxzldeplem  32180  eel0001  32595  eel0000  32596  eel00001  32598  eel00000  32599  e000  32644  e00  32645  bnj1023  32918  bnj1109  32924  bj-mp2c  33208  bj-mp2d  33209  bj-alrimih  33297  diclspsn  35991  dih1dimatlem  36126