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  190  imbi12i  327  pm3.2i  456  sbcom2  2244  sstri  3473  0disj  4416  disjx0  4418  relres  5151  cnvdif  5261  difxp  5280  funopab4  5636  fun0  5658  fvsn  6112  omsinds  6725  reltpos  6989  tpostpos  7004  tpos0  7014  oaabs2  7357  swoer  7402  xpider  7445  erinxp  7448  sbthcl  7703  php  7765  inf0  8135  unctb  8642  fin1a2lem12  8848  axcc2lem  8873  axcclem  8894  brdom3  8963  brdom5  8964  brdom4  8965  pwcfsdom  9015  smobeth  9018  fpwwe2lem8  9069  fpwwe2lem9  9070  fpwwe2lem12  9073  pwxpndom2  9097  pwcdandom  9099  gchac  9113  wunex3  9173  inar1  9207  gruina  9250  ltsopi  9320  recmulnq  9396  prcdnq  9425  ltrel  9703  lerel  9705  suprfinzcl  11057  cnexALT  11305  dfle2  11453  dflt2  11454  uzrdg0i  12179  ltwefz  12183  fzennn  12187  faclbnd4lem1  12484  hashsslei  12602  0csh0  12897  isercolllem1  13727  zsum  13783  sum0  13786  znnen  14264  qnnen  14265  rpnnen  14278  ruc  14294  nthruc  14302  nthruz  14303  phicl2  14715  pwsle  15389  xpsc0  15465  xpsc1  15466  relfull  15812  relfth  15813  gicer  16939  oppglsm  17293  efgrelexlemb  17399  isunit  17884  opsrtoslem2  18707  xrsnsgrp  19003  pjpm  19269  1stcfb  20458  2ndc1stc  20464  2ndcctbss  20468  2ndcdisj2  20470  2ndcsep  20472  hmpher  20797  met1stc  21534  re2ndc  21817  iccpnfhmeo  21971  xrhmeo  21972  xrcmp  21974  xrcon  21975  dyadmbl  22556  opnmblALT  22559  vitalilem2  22565  vitalilem3  22566  vitali  22569  mbfimaopnlem  22609  mbfsup  22618  dgrval  23180  dgrcl  23185  dgrub  23186  dgrlb  23188  aannenlem3  23284  dvrelog  23580  logcn  23590  logccv  23606  logblog  23727  ppiub  24130  lgsquadlem1  24280  lgsquadlem2  24281  dirith2  24364  usgraexmpldifpr  25125  usgraexmplef  25126  disjxwwlks  25462  disjxwwlkn  25471  konigsberg  25713  nvrel  26219  phrel  26454  bnrel  26507  hlrel  26540  pjnormi  27372  lnopunilem1  27661  lnophmlem1  27667  xrge0infssd  28348  xrge0infssdOLD  28349  infxrge0lb  28352  infxrge0lbOLD  28353  infxrge0glb  28354  infxrge0glbOLD  28355  infxrge0gelb  28356  infxrge0gelbOLD  28357  ssnnssfz  28373  xrge0iifiso  28749  omsf  29128  omsfOLD  29132  oms0  29133  omssubaddlem  29135  omssubadd  29136  oms0OLD  29137  omssubaddlemOLD  29139  omssubaddOLD  29140  oddpwdc  29195  bnj1023  29600  bnj1109  29606  erdszelem4  29925  erdszelem8  29929  supfz  30369  inffz  30370  elrn3  30410  trer  30977  fneer  31014  naim1i  31052  naim2i  31053  mont  31074  onpsstopbas  31095  bj-mp2c  31127  bj-mp2d  31128  bj-alrimih  31208  wl-equsal1i  31840  wl-sbcom2d  31855  poimirlem26  31930  mblfinlem1  31941  incsequz2  32042  cncfres  32061  heiborlem3  32109  diclspsn  34731  dih1dimatlem  34866  rencldnfilem  35632  pellexlem4  35646  pellexlem5  35647  ttac  35861  idomsubgmo  36042  areaquad  36071  frege102  36531  lhe4.4ex1a  36648  eel0001  37078  eel0000  37079  eel00001  37081  eel00000  37082  e000  37127  e00  37128  fzisoeu  37472  resincncf  37692  ssnn0ssfz  39751  zlmodzxzldeplem  39912