Theorem mp3an3 1311

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  mp3an13  1313  mp3an23  1314  mp3anl3  1318  opelxp  5018  ov  6395  ovmpt2a  6406  ovmpt2  6411  oaword1  7193  oneo  7222  oeoalem  7237  oeoelem  7239  nnaword1  7270  nnneo  7292  erov  7400  enrefg  7540  f1imaen  7570  mapxpen  7676  acnlem  8420  cdacomen  8552  infmap  8942  canthnumlem  9015  tskin  9126  tsksn  9127  tsk0  9130  gruxp  9174  gruina  9185  genpprecl  9368  addsrpr  9441  mulsrpr  9442  supsrlem  9477  mulid1  9582  00id  9744  mul02lem1  9745  ltneg  10048  leneg  10051  suble0  10062  div1  10232  nnaddcl  10553  nnmulcl  10554  nnge1  10557  nnsub  10570  2halves  10763  halfaddsub  10768  addltmul  10770  zleltp1  10910  nnaddm1cl  10916  zextlt  10933  uzindOLD  10953  eluzp1p1  11107  uzaddcl  11138  znq  11187  xrre  11373  xrre2  11374  fzshftral  11770  fraclt1  11920  expadd  12190  expmul  12193  expubnd  12208  sqmul  12213  bernneq  12274  faclbnd2  12351  faclbnd6  12359  hashgadd  12428  hashun2  12434  hashssdif  12459  hashfun  12479  ccatlcan  12688  ccatrcan  12689  shftval3  12991  sqrlem1  13158  caubnd2  13272  efexp  13918  efival  13969  cos01gt0  14008  odd2np1  14130  divalglem5  14139  gcdmultiple  14272  sqgcd  14280  nn0seqcvgd  14283  phiprmpw  14390  eulerthlem2  14396  odzcllem  14403  omoe  14420  opeo  14421  pythagtriplem15  14437  pythagtriplem17  14439  pcelnn  14477  4sqlem3  14552  xpscfn  15048  fullfunc  15394  fthfunc  15395  prfcl  15671  curf1cl  15696  curfcl  15700  hofcl  15727  odinv  16782  lsmelvalix  16860  dprdval  17229  dprdvalOLD  17231  lsp0  17850  lss0v  17857  coe1scl  18523  zndvds0  18762  frlmlbs  18999  lindfres  19025  lmisfree  19044  ntrin  19729  lpsscls  19809  restperf  19852  txuni2  20232  txopn  20269  elqtop2  20368  xkocnv  20481  ptcmp  20724  xblpnfps  21064  xblpnf  21065  bl2in  21069  unirnblps  21088  unirnbl  21089  blpnfctr  21105  dscopn  21260  bcthlem4  21932  minveclem2  22007  minveclem4  22013  icombl  22140  i1fadd  22268  i1fmul  22269  dvn1  22495  dvexp3  22545  plyconst  22769  plyid  22772  sincosq1eq  23071  sinord  23087  cxpp1  23229  cxpsqrtlem  23251  cxpsqrt  23252  angneg  23334  dcubic  23374  issqf  23608  ppiub  23677  bposlem1  23757  bposlem2  23758  bposlem9  23765  axlowdimlem6  24452  axlowdimlem14  24460  axcontlem2  24470  wwlkn0s  24907  clwwlkn2  24977  rusgranumwlkb0  25155  gx0  25461  gx1  25462  gxm1  25468  gxnn0add  25474  gxnn0mul  25477  ipasslem1  25944  ipasslem2  25945  ipasslem11  25953  minvecolem2  25989  minvecolem3  25990  minvecolem4  25994  shsva  26436  h1datomi  26697  lnfnmuli  27161  leopsq  27246  nmopleid  27256  opsqrlem6  27262  pjnmopi  27265  hstle  27347  csmdsymi  27451  atcvatlem  27502  elsx  28402  dya2iocnrect  28489  cvmliftphtlem  29026  wlimeq12  29615  nofulllem4  29705  fvray  30019  fvline  30022  bpoly2  30047  bpoly3  30048  fsumcube  30050  tan2h  30287  mblfinlem4  30294  mbfresfi  30301  mbfposadd  30302  dvtanlem  30304  itg2addnc  30309  ftc1anclem5  30334  ftc1anclem8  30337  dvasin  30343  tailfb  30435  heiborlem7  30553  igenidl  30700  eldioph4b  30984  diophren  30986  rmxp1  31107  rmyp1  31108  rmxm1  31109  rmym1  31110  wepwso  31227  pfx2  32640  dig0  33481  onetansqsecsq  33545  cotsqcscsq  33546  dpfrac1  33556  atlatmstc  35441  dihglblem2N  37418