Theorem mp3an12 1414

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mp3an12.1	|- ph
mp3an12.2	|- ps
mp3an12.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an12	|- ( ch -> th )

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 |- ps
2		mp3an12.1	. . 3 |- ph
3		mp3an12.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an1 1411	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 4	mpan 706	1 |- ( ch -> th )

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  mp3an12i  1428  ceqsalg  3230  ceqsralv  3234  brelrn  5356  predeq3  5684  funpr  5944  tfi  7053  peano5  7089  wrecseq3  7412  wfr3  7435  oneo  7661  nnneo  7731  fpm  7890  enerOLD  8003  unxpdomlem3  8166  0fsupp  8297  ackbij2  9065  ac6  9302  alephadd  9399  axgroth3  9653  axpre-sup  9990  mul02  10214  cnegex2  10218  addid2  10219  renegcli  10342  div0  10715  divclzi  10760  divcan1zi  10761  divcan2zi  10762  divreczi  10763  divcan3zi  10764  divcan4zi  10765  divasszi  10775  divmulzi  10776  divdirzi  10777  redivclzi  10791  ltm1  10863  mulgt1  10882  recgt1i  10920  recreclt  10922  ltmul1i  10942  ltdiv1i  10943  ltmuldivi  10944  ltmul2i  10945  lemul1i  10946  lemul2i  10947  ledivp1i  10949  ltdivp1i  10950  cju  11016  nnge1  11046  nngt0  11049  nnrecgt0  11058  nnunb  11288  elnnnn0c  11338  elnnz1  11403  recnz  11452  eluzsubi  11715  ge0gtmnf  12003  x2times  12129  xrub  12142  iccen  12317  1mod  12702  m1expcl2  12882  1exp  12889  expubnd  12921  iexpcyc  12969  expnbnd  12993  expnlbnd  12994  faclbnd4lem1  13080  remim  13857  imval2  13891  cjdivi  13931  resqrex  13991  sqrtneglem  14007  absdivzi  14146  iseraltlem2  14413  climcndslem1  14581  climcndslem2  14582  geo2lim  14606  bpoly3  14789  sinhval  14884  coshval  14885  ef01bndlem  14914  sin01gt0  14920  cos01gt0  14921  absefib  14928  efieq1re  14929  evend2  15081  divalglem5  15120  phiprmpw  15481  oddprm  15515  pythagtriplem1  15521  pythagtriplem11  15530  pythagtriplem13  15532  vdwlem13  15697  prmlem1  15814  prmlem2  15827  ress0  15934  frmdplusg  17391  symggen  17890  m1expaddsub  17918  psgnuni  17919  islindf4  20177  resstopn  20990  lecldbas  21023  hmphindis  21600  cnbl0  22577  xrsmopn  22615  zdis  22619  reperflem  22621  xrge0tsms  22637  xrhmeo  22745  oprpiece1res1  22750  cphsqrtcl  22984  ovolicopnf  23292  voliunlem3  23320  volsup  23324  volivth  23375  itg2seq  23509  itg2monolem2  23518  itgz  23547  ibl0  23553  iblss  23571  iblss2  23572  itgss  23578  itgeqa  23580  iblconst  23584  iblabsr  23596  iblmulc2  23597  itgsplit  23602  coeidp  24019  dgrsub  24028  aaliou3lem2  24098  abelth  24195  reeff1olem  24200  pilem3  24207  sincosq1sgn  24250  sincosq3sgn  24252  sincosq4sgn  24253  sineq0  24273  resinf1o  24282  efif1olem4  24291  logdivlti  24366  logdivlt  24367  efopn  24404  1cxp  24418  ecxp  24419  cxpsqrt  24449  isosctrlem1  24548  sinasin  24616  asinsin  24619  log2cnv  24671  basellem2  24808  basellem3  24809  isnsqf  24861  ppidif  24889  ppiublem1  24927  chtub  24937  efexple  25006  bposlem6  25014  bposlem8  25016  lgsdir2lem2  25051  2sqb  25157  ostth3  25327  axpaschlem  25820  axlowdimlem3  25824  axlowdimlem7  25828  axlowdimlem9  25830  axlowdimlem12  25833  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  sizusglecusg  26359  imsmetlem  27545  nmoubi  27627  nmobndi  27630  nmounbi  27631  nmlno0lem  27648  nmlnoubi  27651  isblo3i  27656  blometi  27658  blocni  27660  blocn2  27663  ipasslem2  27687  siii  27708  ubthlem1  27726  ubthlem2  27727  ubthlem3  27728  htthlem  27774  hvsubid  27883  hv2times  27918  hi01  27953  hhssabloilem  28118  pjsumi  28569  mayete3i  28587  hoaddcomi  28631  hodsi  28634  hoaddassi  28635  hocadddiri  28638  hocsubdiri  28639  hoaddid1i  28645  honegsubi  28655  honegneg  28665  ho2times  28678  eigrei  28693  eigorthi  28696  nmopnegi  28824  hoddii  28848  lnophsi  28860  lnopeqi  28867  nmoptrii  28953  opsqrlem1  28999  opsqrlem6  29004  pjsdii  29014  pjddii  29015  pjscji  29029  pjssposi  29031  pjssdif2i  29033  pjtoi  29038  mdsl2bi  29182  cvmdi  29183  mdslmd3i  29191  mdslmd4i  29192  mdexchi  29194  cvati  29225  cvexchlem  29227  mdsymi  29270  dmdbr5ati  29281  cdj1i  29292  cdj3lem1  29293  xrge0infss  29525  xrge0tsmsd  29785  rrhre  30065  esumpinfval  30135  oms0  30359  eulerpartlems  30422  eulerpartlemgf  30441  probmeasb  30492  cvmliftlem5  31271  bcneg1  31622  wsuceq3  31763  scutun12  31917  fullfunfv  32054  finminlem  32312  nn0prpwlem  32317  bj-ceqsalg0  32877  bj-ceqsalgALT  32879  bj-ceqsalgvALT  32881  bj-vtoclgfALT  33021  finxpreclem4  33231  sin2h  33399  cos2h  33400  tan2h  33401  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem30  33439  poimirlem32  33441  poimir  33442  broucube  33443  mblfinlem1  33446  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  volsupnfl  33454  itg2addnclem3  33463  iblmulc2nc  33475  ftc1anc  33493  dvasin  33496  heiborlem3  33612  heiborlem6  33615  heiborlem8  33617  cdleme32fva  35725  isnumbasgrplem1  37671  areaquad  37802  binomcxplemnotnn0  38555  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  m1mod0mod1  41339  sgoldbeven3prm  41671  aacllem  42547