Theorem mp3an3 1296

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

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

Assertion

Ref	Expression
mp3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expia 1182	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 17	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 958

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 185  df-an 371  df-3an 960

This theorem is referenced by:  mp3an13  1298  mp3an23  1299  mp3anl3  1303  opelxp  4856  ov  6199  ovmpt2a  6210  ovmpt2  6215  oaword1  6979  oneo  7008  oeoalem  7023  oeoelem  7025  nnaword1  7056  nnneo  7078  erov  7185  th3q  7197  enrefg  7329  f1imaen  7359  mapxpen  7465  acnlem  8206  cdacomen  8338  infmap  8728  canthnumlem  8802  tskin  8913  tsksn  8914  tsk0  8917  gruxp  8961  gruina  8972  genpprecl  9157  supsrlem  9265  mulid1  9370  00id  9531  mul02lem1  9532  ltneg  9826  leneg  9829  suble0  9840  div1  10010  nnaddcl  10331  nnmulcl  10332  nnge1  10335  nnsub  10347  2halves  10540  halfaddsub  10545  addltmul  10547  zleltp1  10682  nnaddm1cl  10688  zextlt  10703  uzindOLD  10723  eluzp1p1  10873  uzaddcl  10898  znq  10944  xrre  11128  xrre2  11129  fzshftral  11530  fraclt1  11635  expadd  11889  expmul  11892  expubnd  11907  sqmul  11912  bernneq  11973  faclbnd2  12050  faclbnd6  12058  hashgadd  12123  hashun2  12129  hashssdif  12150  hashfun  12182  ccatlcan  12349  ccatrcan  12350  shftval3  12548  sqrlem1  12715  caubnd2  12828  efexp  13367  efival  13418  cos01gt0  13457  odd2np1  13574  divalglem5  13583  gcdmultiple  13716  sqgcd  13724  nn0seqcvgd  13727  phiprmpw  13833  eulerthlem2  13839  odzcllem  13846  omoe  13861  opeo  13862  pythagtriplem15  13878  pythagtriplem17  13880  pcelnn  13918  4sqlem3  13993  xpscfn  14479  fullfunc  14798  fthfunc  14799  prfcl  14995  curf1cl  15020  curfcl  15024  hofcl  15051  odinv  16041  lsmelvalix  16119  dprdval  16458  dprdvalOLD  16460  lsp0  17011  lss0v  17018  coe1scl  17636  zndvds0  17824  frlmlbs  18066  lindfres  18093  lmisfree  18112  ntrin  18506  lpsscls  18586  restperf  18629  txuni2  18979  txopn  19016  elqtop2  19115  xkocnv  19228  ptcmp  19471  xblpnfps  19811  xblpnf  19812  bl2in  19816  unirnblps  19835  unirnbl  19836  blpnfctr  19852  dscopn  20007  bcthlem4  20679  minveclem2  20754  minveclem4  20760  icombl  20886  i1fadd  21014  i1fmul  21015  dvn1  21241  dvexp3  21291  plyconst  21558  plyid  21561  sincosq1eq  21858  sinord  21874  cxpp1  22009  cxpsqrlem  22031  cxpsqr  22032  angneg  22083  dcubic  22125  issqf  22358  ppiub  22427  bposlem1  22507  bposlem2  22508  bposlem9  22515  axlowdimlem6  23015  axlowdimlem14  23023  axcontlem2  23033  gx0  23570  gx1  23571  gxm1  23577  gxnn0add  23583  gxnn0mul  23586  ipasslem1  24053  ipasslem2  24054  ipasslem11  24062  minvecolem2  24098  minvecolem3  24099  minvecolem4  24103  shsva  24545  h1datomi  24806  lnfnmuli  25270  leopsq  25355  nmopleid  25365  opsqrlem6  25371  pjnmopi  25374  hstle  25456  csmdsymi  25560  atcvatlem  25611  elsx  26461  dya2iocnrect  26549  cvmliftphtlem  27053  wlimeq12  27602  nofulllem4  27692  fvray  28018  fvline  28021  bpoly2  28046  bpoly3  28047  fsumcube  28049  tan2h  28265  mblfinlem4  28272  mbfresfi  28279  mbfposadd  28280  dvtanlem  28282  itg2addnc  28287  ftc1anclem5  28312  ftc1anclem8  28315  dvasin  28321  tailfb  28439  heiborlem7  28557  igenidl  28704  eldioph4b  28992  diophren  28994  rmxp1  29115  rmyp1  29116  rmxm1  29117  rmym1  29118  wepwso  29237  wwlkn0s  30182  clwwlkn2  30281  rusgranumwlkb0  30414  onetansqsecsq  30802  cotsqcscsq  30803  dpfrac1  30813  atlatmstc  32534  dihglblem2N  34509