Theorem mp3an3 1313

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 1198	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 17	1 |- ( ( ph /\ ps ) -> th )

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

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 975

This theorem is referenced by:  mp3an13  1315  mp3an23  1316  mp3anl3  1320  opelxp  5028  ov  6404  ovmpt2a  6415  ovmpt2  6420  oaword1  7198  oneo  7227  oeoalem  7242  oeoelem  7244  nnaword1  7275  nnneo  7297  erov  7405  enrefg  7544  f1imaen  7574  mapxpen  7680  acnlem  8425  cdacomen  8557  infmap  8947  canthnumlem  9022  tskin  9133  tsksn  9134  tsk0  9137  gruxp  9181  gruina  9192  genpprecl  9375  addsrpr  9448  mulsrpr  9449  supsrlem  9484  mulid1  9589  00id  9750  mul02lem1  9751  ltneg  10048  leneg  10051  suble0  10062  div1  10232  nnaddcl  10554  nnmulcl  10555  nnge1  10558  nnsub  10570  2halves  10763  halfaddsub  10768  addltmul  10770  zleltp1  10909  nnaddm1cl  10915  zextlt  10931  uzindOLD  10951  eluzp1p1  11103  uzaddcl  11133  znq  11182  xrre  11366  xrre2  11367  fzshftral  11761  fraclt1  11903  expadd  12172  expmul  12175  expubnd  12190  sqmul  12195  bernneq  12256  faclbnd2  12333  faclbnd6  12341  hashgadd  12409  hashun2  12415  hashssdif  12436  hashfun  12457  ccatlcan  12656  ccatrcan  12657  shftval3  12868  sqrlem1  13035  caubnd2  13149  efexp  13693  efival  13744  cos01gt0  13783  odd2np1  13901  divalglem5  13910  gcdmultiple  14043  sqgcd  14051  nn0seqcvgd  14054  phiprmpw  14161  eulerthlem2  14167  odzcllem  14174  omoe  14191  opeo  14192  pythagtriplem15  14208  pythagtriplem17  14210  pcelnn  14248  4sqlem3  14323  xpscfn  14810  fullfunc  15129  fthfunc  15130  prfcl  15326  curf1cl  15351  curfcl  15355  hofcl  15382  odinv  16379  lsmelvalix  16457  dprdval  16825  dprdvalOLD  16827  lsp0  17438  lss0v  17445  coe1scl  18099  zndvds0  18356  frlmlbs  18598  lindfres  18625  lmisfree  18644  ntrin  19328  lpsscls  19408  restperf  19451  txuni2  19801  txopn  19838  elqtop2  19937  xkocnv  20050  ptcmp  20293  xblpnfps  20633  xblpnf  20634  bl2in  20638  unirnblps  20657  unirnbl  20658  blpnfctr  20674  dscopn  20829  bcthlem4  21501  minveclem2  21576  minveclem4  21582  icombl  21709  i1fadd  21837  i1fmul  21838  dvn1  22064  dvexp3  22114  plyconst  22338  plyid  22341  sincosq1eq  22638  sinord  22654  cxpp1  22789  cxpsqrtlem  22811  cxpsqrt  22812  angneg  22863  dcubic  22905  issqf  23138  ppiub  23207  bposlem1  23287  bposlem2  23288  bposlem9  23295  axlowdimlem6  23926  axlowdimlem14  23934  axcontlem2  23944  wwlkn0s  24381  clwwlkn2  24451  rusgranumwlkb0  24629  gx0  24939  gx1  24940  gxm1  24946  gxnn0add  24952  gxnn0mul  24955  ipasslem1  25422  ipasslem2  25423  ipasslem11  25431  minvecolem2  25467  minvecolem3  25468  minvecolem4  25472  shsva  25914  h1datomi  26175  lnfnmuli  26639  leopsq  26724  nmopleid  26734  opsqrlem6  26740  pjnmopi  26743  hstle  26825  csmdsymi  26929  atcvatlem  26980  elsx  27805  dya2iocnrect  27892  cvmliftphtlem  28402  wlimeq12  28952  nofulllem4  29042  fvray  29368  fvline  29371  bpoly2  29396  bpoly3  29397  fsumcube  29399  tan2h  29624  mblfinlem4  29631  mbfresfi  29638  mbfposadd  29639  dvtanlem  29641  itg2addnc  29646  ftc1anclem5  29671  ftc1anclem8  29674  dvasin  29680  tailfb  29798  heiborlem7  29916  igenidl  30063  eldioph4b  30349  diophren  30351  rmxp1  30472  rmyp1  30473  rmxm1  30474  rmym1  30475  wepwso  30592  onetansqsecsq  32236  cotsqcscsq  32237  dpfrac1  32247  atlatmstc  34116  dihglblem2N  36091