Theorem mp3an3 1413

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

Syntax hints:   -> wi 4   /\ wa 384   /\ 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:  mp3an13  1415  mp3an23  1416  mp3anl3  1420  opelxp  5146  ov  6780  ovmpt2a  6791  ovmpt2  6796  oaword1  7632  oneo  7661  oeoalem  7676  oeoelem  7678  nnaword1  7709  nnneo  7731  erov  7844  enrefg  7987  f1imaen  8018  mapxpen  8126  acnlem  8871  cdacomen  9003  infmap  9398  canthnumlem  9470  tskin  9581  tsksn  9582  tsk0  9585  gruxp  9629  gruina  9640  genpprecl  9823  addsrpr  9896  mulsrpr  9897  supsrlem  9932  mulid1  10037  00id  10211  mul02lem1  10212  ltneg  10528  leneg  10531  suble0  10542  div1  10716  nnaddcl  11042  nnmulcl  11043  nnge1  11046  nnsub  11059  2halves  11260  halfaddsub  11265  addltmul  11268  zleltp1  11428  nnaddm1cl  11434  zextlt  11451  eluzp1p1  11713  uzaddcl  11744  znq  11792  xrre  12000  xrre2  12001  fzshftral  12428  fraclt1  12603  expadd  12902  expmul  12905  expubnd  12921  sqmul  12926  bernneq  12990  faclbnd2  13078  faclbnd6  13086  hashgadd  13166  hashun2  13172  hashssdif  13200  hashfun  13224  ccatlcan  13472  ccatrcan  13473  shftval3  13816  sqrlem1  13983  caubnd2  14097  bpoly2  14788  bpoly3  14789  fsumcube  14791  efexp  14831  efival  14882  cos01gt0  14921  odd2np1  15065  halfleoddlt  15086  omoe  15088  opeo  15089  divalglem5  15120  gcdmultiple  15269  sqgcd  15278  nn0seqcvgd  15283  phiprmpw  15481  eulerthlem2  15487  odzcllem  15497  pythagtriplem15  15534  pythagtriplem17  15536  pcelnn  15574  4sqlem3  15654  xpscfn  16219  fullfunc  16566  fthfunc  16567  prfcl  16843  curf1cl  16868  curfcl  16872  hofcl  16899  odinv  17978  lsmelvalix  18056  dprdval  18402  lsp0  19009  lss0v  19016  coe1scl  19657  zndvds0  19899  frlmlbs  20136  lindfres  20162  lmisfree  20181  ntrin  20865  lpsscls  20945  restperf  20988  txuni2  21368  txopn  21405  elqtop2  21504  xkocnv  21617  ptcmp  21862  xblpnfps  22200  xblpnf  22201  bl2in  22205  unirnblps  22224  unirnbl  22225  blpnfctr  22241  dscopn  22378  bcthlem4  23124  minveclem2  23197  minveclem4  23203  icombl  23332  i1fadd  23462  i1fmul  23463  dvn1  23689  dvexp3  23741  plyconst  23962  plyid  23965  sincosq1eq  24264  sinord  24280  cxpp1  24426  cxpsqrtlem  24448  cxpsqrt  24449  angneg  24533  dcubic  24573  issqf  24862  ppiub  24929  bposlem1  25009  bposlem2  25010  bposlem9  25017  axlowdimlem6  25827  axlowdimlem14  25835  axcontlem2  25845  structgrssvtxlemOLD  25915  pthdlem2  26664  0ewlk  26975  ipasslem1  27686  ipasslem2  27687  ipasslem11  27695  minvecolem2  27731  minvecolem3  27732  minvecolem4  27736  shsva  28179  h1datomi  28440  lnfnmuli  28903  leopsq  28988  nmopleid  28998  opsqrlem6  29004  pjnmopi  29007  hstle  29089  csmdsymi  29193  atcvatlem  29244  dpfrac1  29599  dpfrac1OLD  29600  elsx  30257  dya2iocnrect  30343  cvmliftphtlem  31299  wlimeq12  31765  nosupno  31849  nosupfv  31852  scutval  31911  scutun12  31917  fvray  32248  fvline  32251  tailfb  32372  uncov  33390  tan2h  33401  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem32  33441  mblfinlem4  33449  mbfresfi  33456  mbfposadd  33457  itg2addnc  33464  ftc1anclem5  33489  ftc1anclem8  33492  dvasin  33496  heiborlem7  33616  igenidl  33862  el3v3  33990  atlatmstc  34606  dihglblem2N  36583  eldioph4b  37375  diophren  37377  rmxp1  37497  rmyp1  37498  rmxm1  37499  rmym1  37500  wepwso  37613  pfx2  41412  dig0  42400  onetansqsecsq  42502  cotsqcscsq  42503