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  2160  sstri  3472  0disj  4392  disjx0  4394  relres  5245  cnvdif  5350  difxp  5369  funopab4  5560  fun0  5582  fvsn  6019  reltpos  6859  tpostpos  6874  tpos0  6884  oaabs2  7193  swoer  7238  xpider  7280  erinxp  7283  sbthcl  7542  php  7604  inf0  7937  unctb  8484  fin1a2lem12  8690  axcc2lem  8715  axcclem  8736  brdom3  8805  brdom5  8806  brdom4  8807  pwcfsdom  8857  smobeth  8860  fpwwe2lem8  8914  fpwwe2lem9  8915  fpwwe2lem12  8918  pwxpndom2  8942  pwcdandom  8944  gchac  8958  wunex3  9018  inar1  9052  gruina  9095  ltsopi  9167  recmulnq  9243  prcdnq  9272  ltrel  9549  lerel  9551  cnexALT  11097  dfle2  11234  dflt2  11235  uzrdg0i  11898  ltwefz  11902  fzennn  11906  faclbnd4lem1  12185  hashsslei  12293  0csh0  12547  isercolllem1  13259  zsum  13312  sum0  13315  xpnnenOLD  13609  znnen  13612  qnnen  13613  rpnnen  13626  ruc  13642  nthruc  13650  nthruz  13651  phicl2  13960  pwsle  14548  xpsc0  14616  xpsc1  14617  relfull  14936  relfth  14937  gicer  15922  oppglsm  16261  efgrelexlemb  16367  isunit  16871  opsrtoslem2  17689  pjpm  18257  1stcfb  19180  2ndc1stc  19186  2ndcctbss  19190  2ndcdisj2  19192  2ndcsep  19194  hmpher  19488  met1stc  20227  re2ndc  20509  iccpnfhmeo  20648  xrhmeo  20649  xrcmp  20651  xrcon  20652  dyadmbl  21212  opnmblALT  21215  vitalilem2  21221  vitalilem3  21222  vitali  21225  mbfimaopnlem  21265  mbfsup  21274  dgrval  21828  dgrcl  21833  dgrub  21834  dgrlb  21836  aannenlem3  21928  dvrelog  22214  logcn  22224  logccv  22240  ppiub  22675  lgsquadlem1  22825  lgsquadlem2  22826  dirith2  22909  usgraexmpldifpr  23469  usgraexmpl  23470  konigsberg  23759  nvrel  24131  phrel  24366  bnrel  24419  hlrel  24442  pjnormi  25275  lnopunilem1  25565  lnophmlem1  25571  xrge0infssd  26204  ssnnssfz  26220  xrge0iifiso  26509  oms0  26853  oddpwdc  26880  erdszelem4  27225  erdszelem8  27229  supfz  27529  inffz  27530  elrn3  27716  omsinds  27823  naim1i  28376  naim2i  28377  mont  28398  onpsstopbas  28419  wl-equsal1i  28519  wl-sbcom2d  28534  mblfinlem1  28575  trer  28658  fneer  28707  incsequz2  28792  cncfres  28811  heiborlem3  28859  rencldnfilem  29306  pellexlem4  29320  pellexlem5  29321  ttac  29532  idomsubgmo  29710  areaquad  29739  lhe4.4ex1a  29750  disjxwwlks  30515  disjxwwlkn  30711  ssnn0ssfz  30888  suprfinzcl  30892  zlmodzxzldeplem  31158  eel0001  31768  eel0000  31769  eel00001  31771  eel00000  31772  e000  31817  e00  31818  bnj1023  32091  bnj1109  32097  bj-mp2c  32381  bj-mp2d  32382  bj-alrimih  32468  diclspsn  35162  dih1dimatlem  35297