Theorem mp3an3 1304

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

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

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 967

This theorem is referenced by:  mp3an13  1306  mp3an23  1307  mp3anl3  1311  opelxp  4970  ov  6313  ovmpt2a  6324  ovmpt2  6329  oaword1  7094  oneo  7123  oeoalem  7138  oeoelem  7140  nnaword1  7171  nnneo  7193  erov  7300  th3q  7312  enrefg  7444  f1imaen  7474  mapxpen  7580  acnlem  8322  cdacomen  8454  infmap  8844  canthnumlem  8919  tskin  9030  tsksn  9031  tsk0  9034  gruxp  9078  gruina  9089  genpprecl  9274  supsrlem  9382  mulid1  9487  00id  9648  mul02lem1  9649  ltneg  9943  leneg  9946  suble0  9957  div1  10127  nnaddcl  10448  nnmulcl  10449  nnge1  10452  nnsub  10464  2halves  10657  halfaddsub  10662  addltmul  10664  zleltp1  10799  nnaddm1cl  10805  zextlt  10820  uzindOLD  10840  eluzp1p1  10990  uzaddcl  11015  znq  11061  xrre  11245  xrre2  11246  fzshftral  11657  fraclt1  11762  expadd  12016  expmul  12019  expubnd  12034  sqmul  12039  bernneq  12100  faclbnd2  12177  faclbnd6  12185  hashgadd  12251  hashun2  12257  hashssdif  12278  hashfun  12310  ccatlcan  12477  ccatrcan  12478  shftval3  12676  sqrlem1  12843  caubnd2  12956  efexp  13496  efival  13547  cos01gt0  13586  odd2np1  13703  divalglem5  13712  gcdmultiple  13845  sqgcd  13853  nn0seqcvgd  13856  phiprmpw  13962  eulerthlem2  13968  odzcllem  13975  omoe  13990  opeo  13991  pythagtriplem15  14007  pythagtriplem17  14009  pcelnn  14047  4sqlem3  14122  xpscfn  14608  fullfunc  14927  fthfunc  14928  prfcl  15124  curf1cl  15149  curfcl  15153  hofcl  15180  odinv  16175  lsmelvalix  16253  dprdval  16599  dprdvalOLD  16601  lsp0  17205  lss0v  17212  coe1scl  17857  zndvds0  18101  frlmlbs  18343  lindfres  18370  lmisfree  18389  ntrin  18790  lpsscls  18870  restperf  18913  txuni2  19263  txopn  19300  elqtop2  19399  xkocnv  19512  ptcmp  19755  xblpnfps  20095  xblpnf  20096  bl2in  20100  unirnblps  20119  unirnbl  20120  blpnfctr  20136  dscopn  20291  bcthlem4  20963  minveclem2  21038  minveclem4  21044  icombl  21171  i1fadd  21299  i1fmul  21300  dvn1  21526  dvexp3  21576  plyconst  21800  plyid  21803  sincosq1eq  22100  sinord  22116  cxpp1  22251  cxpsqrlem  22273  cxpsqr  22274  angneg  22325  dcubic  22367  issqf  22600  ppiub  22669  bposlem1  22749  bposlem2  22750  bposlem9  22757  axlowdimlem6  23338  axlowdimlem14  23346  axcontlem2  23356  gx0  23893  gx1  23894  gxm1  23900  gxnn0add  23906  gxnn0mul  23909  ipasslem1  24376  ipasslem2  24377  ipasslem11  24385  minvecolem2  24421  minvecolem3  24422  minvecolem4  24426  shsva  24868  h1datomi  25129  lnfnmuli  25593  leopsq  25678  nmopleid  25688  opsqrlem6  25694  pjnmopi  25697  hstle  25779  csmdsymi  25883  atcvatlem  25934  elsx  26746  dya2iocnrect  26833  cvmliftphtlem  27343  wlimeq12  27893  nofulllem4  27983  fvray  28309  fvline  28312  bpoly2  28337  bpoly3  28338  fsumcube  28340  tan2h  28565  mblfinlem4  28572  mbfresfi  28579  mbfposadd  28580  dvtanlem  28582  itg2addnc  28587  ftc1anclem5  28612  ftc1anclem8  28615  dvasin  28621  tailfb  28739  heiborlem7  28857  igenidl  29004  eldioph4b  29291  diophren  29293  rmxp1  29414  rmyp1  29415  rmxm1  29416  rmym1  29417  wepwso  29536  wwlkn0s  30480  clwwlkn2  30579  rusgranumwlkb0  30712  onetansqsecsq  31395  cotsqcscsq  31396  dpfrac1  31406  atlatmstc  33273  dihglblem2N  35248