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  2151  sstri  3360  0disj  4280  disjx0  4282  relres  5133  cnvdif  5238  difxp  5257  funopab4  5448  fun0  5470  fvsn  5906  reltpos  6745  tpostpos  6760  tpos0  6770  oaabs2  7076  swoer  7121  xpider  7163  erinxp  7166  sbthcl  7425  php  7487  inf0  7819  unctb  8366  fin1a2lem12  8572  axcc2lem  8597  axcclem  8618  brdom3  8687  brdom5  8688  brdom4  8689  pwcfsdom  8739  smobeth  8742  fpwwe2lem8  8796  fpwwe2lem9  8797  fpwwe2lem12  8800  pwxpndom2  8824  pwcdandom  8826  gchac  8840  wunex3  8900  inar1  8934  gruina  8977  ltsopi  9049  recmulnq  9125  prcdnq  9154  ltrel  9431  lerel  9433  cnexALT  10979  dfle2  11116  dflt2  11117  uzrdg0i  11774  ltwefz  11778  fzennn  11782  faclbnd4lem1  12061  hashsslei  12168  0csh0  12422  isercolllem1  13134  zsum  13187  sum0  13190  xpnnenOLD  13484  znnen  13487  qnnen  13488  rpnnen  13501  ruc  13517  nthruc  13525  nthruz  13526  phicl2  13835  pwsle  14422  xpsc0  14490  xpsc1  14491  relfull  14810  relfth  14811  gicer  15795  oppglsm  16132  efgrelexlemb  16238  isunit  16737  opsrtoslem2  17541  pjpm  18108  1stcfb  19024  2ndc1stc  19030  2ndcctbss  19034  2ndcdisj2  19036  2ndcsep  19038  hmpher  19332  met1stc  20071  re2ndc  20353  iccpnfhmeo  20492  xrhmeo  20493  xrcmp  20495  xrcon  20496  dyadmbl  21055  opnmblALT  21058  vitalilem2  21064  vitalilem3  21065  vitali  21068  mbfimaopnlem  21108  mbfsup  21117  dgrval  21671  dgrcl  21676  dgrub  21677  dgrlb  21679  aannenlem3  21771  dvrelog  22057  logcn  22067  logccv  22083  ppiub  22518  lgsquadlem1  22668  lgsquadlem2  22669  dirith2  22752  usgraexmpldifpr  23269  usgraexmpl  23270  konigsberg  23559  nvrel  23931  phrel  24166  bnrel  24219  hlrel  24242  pjnormi  25075  lnopunilem1  25365  lnophmlem1  25371  xrge0infssd  26005  ssnnssfz  26027  xrge0iifiso  26317  oms0  26662  oddpwdc  26689  erdszelem4  27034  erdszelem8  27038  supfz  27337  inffz  27338  elrn3  27524  omsinds  27631  naim1i  28184  naim2i  28185  mont  28207  onpsstopbas  28228  wl-equsal1i  28323  wl-sbcom2d  28338  mblfinlem1  28381  trer  28464  fneer  28513  incsequz2  28598  cncfres  28617  heiborlem3  28665  rencldnfilem  29112  pellexlem4  29126  pellexlem5  29127  ttac  29338  idomsubgmo  29516  areaquad  29545  lhe4.4ex1a  29556  disjxwwlks  30321  disjxwwlkn  30517  ssnn0ssfz  30693  suprfinzcl  30696  zlmodzxzldeplem  30929  eel0001  31338  eel0000  31339  eel00001  31341  eel00000  31342  e000  31387  e00  31388  bnj1023  31661  bnj1109  31667  bj-mp2c  31951  bj-mp2d  31952  bj-alrimih  32030  diclspsn  34679  dih1dimatlem  34814