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  452  sbcom2  2153  sstri  3353  0disj  4273  disjx0  4275  relres  5126  cnvdif  5231  difxp  5250  funopab4  5441  fun0  5463  fvsn  5898  reltpos  6739  tpostpos  6754  tpos0  6764  oaabs2  7072  swoer  7117  xpider  7159  erinxp  7162  sbthcl  7421  php  7483  inf0  7815  unctb  8362  fin1a2lem12  8568  axcc2lem  8593  axcclem  8614  brdom3  8683  brdom5  8684  brdom4  8685  pwcfsdom  8735  smobeth  8738  fpwwe2lem8  8792  fpwwe2lem9  8793  fpwwe2lem12  8796  pwxpndom2  8820  pwcdandom  8822  gchac  8836  wunex3  8896  inar1  8930  gruina  8973  ltsopi  9045  recmulnq  9121  prcdnq  9150  ltrel  9427  lerel  9429  cnexALT  10975  dfle2  11112  dflt2  11113  uzrdg0i  11766  ltwefz  11770  fzennn  11774  faclbnd4lem1  12053  hashsslei  12160  0csh0  12414  isercolllem1  13126  zsum  13179  sum0  13182  xpnnenOLD  13475  znnen  13478  qnnen  13479  rpnnen  13492  ruc  13508  nthruc  13516  nthruz  13517  phicl2  13826  pwsle  14413  xpsc0  14481  xpsc1  14482  relfull  14801  relfth  14802  gicer  15784  oppglsm  16121  efgrelexlemb  16227  isunit  16683  opsrtoslem2  17498  pjpm  17975  1stcfb  18891  2ndc1stc  18897  2ndcctbss  18901  2ndcdisj2  18903  2ndcsep  18905  hmpher  19199  met1stc  19938  re2ndc  20220  iccpnfhmeo  20359  xrhmeo  20360  xrcmp  20362  xrcon  20363  dyadmbl  20922  opnmblALT  20925  vitalilem2  20931  vitalilem3  20932  vitali  20935  mbfimaopnlem  20975  mbfsup  20984  dgrval  21581  dgrcl  21586  dgrub  21587  dgrlb  21589  aannenlem3  21681  dvrelog  21967  logcn  21977  logccv  21993  ppiub  22428  lgsquadlem1  22578  lgsquadlem2  22579  dirith2  22662  usgraexmpldifpr  23141  usgraexmpl  23142  konigsberg  23431  nvrel  23803  phrel  24038  bnrel  24091  hlrel  24114  pjnormi  24947  lnopunilem1  25237  lnophmlem1  25243  ssnnssfz  25899  xrge0iifiso  26219  oddpwdc  26585  erdszelem4  26930  erdszelem8  26934  supfz  27233  inffz  27234  elrn3  27420  omsinds  27527  naim1i  28080  naim2i  28081  mont  28103  onpsstopbas  28124  wl-equsal1i  28220  wl-sbcom2d  28235  mblfinlem1  28272  trer  28355  fneer  28404  incsequz2  28489  cncfres  28508  heiborlem3  28556  rencldnfilem  29004  pellexlem4  29018  pellexlem5  29019  ttac  29230  idomsubgmo  29408  areaquad  29437  lhe4.4ex1a  29448  disjxwwlks  30214  disjxwwlkn  30410  zlmodzxzldeplem  30770  eel0001  31174  eel0000  31175  eel00001  31177  eel00000  31178  e000  31223  e00  31224  bnj1023  31497  bnj1109  31503  diclspsn  34433  dih1dimatlem  34568