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  2241  sstri  3479  0disj  4419  disjx0  4421  relres  5152  cnvdif  5262  difxp  5281  funopab4  5636  fun0  5658  fvsn  6112  omsinds  6725  reltpos  6986  tpostpos  7001  tpos0  7011  oaabs2  7354  swoer  7399  xpider  7442  erinxp  7445  sbthcl  7700  php  7762  inf0  8126  unctb  8633  fin1a2lem12  8839  axcc2lem  8864  axcclem  8885  brdom3  8954  brdom5  8955  brdom4  8956  pwcfsdom  9006  smobeth  9009  fpwwe2lem8  9061  fpwwe2lem9  9062  fpwwe2lem12  9065  pwxpndom2  9089  pwcdandom  9091  gchac  9105  wunex3  9165  inar1  9199  gruina  9242  ltsopi  9312  recmulnq  9388  prcdnq  9417  ltrel  9695  lerel  9697  suprfinzcl  11050  cnexALT  11298  dfle2  11446  dflt2  11447  uzrdg0i  12170  ltwefz  12174  fzennn  12178  faclbnd4lem1  12475  hashsslei  12593  0csh0  12880  isercolllem1  13706  zsum  13762  sum0  13765  znnen  14243  qnnen  14244  rpnnen  14257  ruc  14273  nthruc  14281  nthruz  14282  phicl2  14685  pwsle  15349  xpsc0  15417  xpsc1  15418  relfull  15764  relfth  15765  gicer  16891  oppglsm  17229  efgrelexlemb  17335  isunit  17820  opsrtoslem2  18643  xrsnsgrp  18939  pjpm  19202  1stcfb  20391  2ndc1stc  20397  2ndcctbss  20401  2ndcdisj2  20403  2ndcsep  20405  hmpher  20730  met1stc  21467  re2ndc  21730  iccpnfhmeo  21869  xrhmeo  21870  xrcmp  21872  xrcon  21873  dyadmbl  22435  opnmblALT  22438  vitalilem2  22444  vitalilem3  22445  vitali  22448  mbfimaopnlem  22488  mbfsup  22497  dgrval  23050  dgrcl  23055  dgrub  23056  dgrlb  23058  aannenlem3  23151  dvrelog  23447  logcn  23457  logccv  23473  logblog  23594  ppiub  23995  lgsquadlem1  24145  lgsquadlem2  24146  dirith2  24229  usgraexmpldifpr  24973  usgraexmpl  24974  disjxwwlks  25309  disjxwwlkn  25318  konigsberg  25560  nvrel  26066  phrel  26301  bnrel  26354  hlrel  26377  pjnormi  27209  lnopunilem1  27498  lnophmlem1  27504  xrge0infssd  28182  infxrge0lb  28185  infxrge0glb  28186  infxrge0gelb  28187  ssnnssfz  28203  xrge0iifiso  28580  omsf  28957  oms0  28958  omssubaddlem  28960  omssubadd  28961  oddpwdc  29013  bnj1023  29380  bnj1109  29386  erdszelem4  29705  erdszelem8  29709  supfz  30149  inffz  30150  elrn3  30190  trer  30757  fneer  30794  naim1i  30832  naim2i  30833  mont  30854  onpsstopbas  30875  bj-mp2c  30907  bj-mp2d  30908  bj-alrimih  30988  wl-equsal1i  31583  wl-sbcom2d  31598  poimirlem26  31669  mblfinlem1  31680  incsequz2  31781  cncfres  31800  heiborlem3  31848  diclspsn  34470  dih1dimatlem  34605  rencldnfilem  35371  pellexlem4  35385  pellexlem5  35386  ttac  35596  idomsubgmo  35770  areaquad  35799  frege102  36197  lhe4.4ex1a  36314  eel0001  36744  eel0000  36745  eel00001  36747  eel00000  36748  e000  36793  e00  36794  fzisoeu  37126  resincncf  37323  ssnn0ssfz  38889  zlmodzxzldeplem  39050