Theorem mp3an3 1303

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 1189	. 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  1305  mp3an23  1306  mp3anl3  1310  opelxp  4864  ov  6205  ovmpt2a  6216  ovmpt2  6221  oaword1  6983  oneo  7012  oeoalem  7027  oeoelem  7029  nnaword1  7060  nnneo  7082  erov  7189  th3q  7201  enrefg  7333  f1imaen  7363  mapxpen  7469  acnlem  8210  cdacomen  8342  infmap  8732  canthnumlem  8807  tskin  8918  tsksn  8919  tsk0  8922  gruxp  8966  gruina  8977  genpprecl  9162  supsrlem  9270  mulid1  9375  00id  9536  mul02lem1  9537  ltneg  9831  leneg  9834  suble0  9845  div1  10015  nnaddcl  10336  nnmulcl  10337  nnge1  10340  nnsub  10352  2halves  10545  halfaddsub  10550  addltmul  10552  zleltp1  10687  nnaddm1cl  10693  zextlt  10708  uzindOLD  10728  eluzp1p1  10878  uzaddcl  10903  znq  10949  xrre  11133  xrre2  11134  fzshftral  11539  fraclt1  11644  expadd  11898  expmul  11901  expubnd  11916  sqmul  11921  bernneq  11982  faclbnd2  12059  faclbnd6  12067  hashgadd  12132  hashun2  12138  hashssdif  12159  hashfun  12191  ccatlcan  12358  ccatrcan  12359  shftval3  12557  sqrlem1  12724  caubnd2  12837  efexp  13377  efival  13428  cos01gt0  13467  odd2np1  13584  divalglem5  13593  gcdmultiple  13726  sqgcd  13734  nn0seqcvgd  13737  phiprmpw  13843  eulerthlem2  13849  odzcllem  13856  omoe  13871  opeo  13872  pythagtriplem15  13888  pythagtriplem17  13890  pcelnn  13928  4sqlem3  14003  xpscfn  14489  fullfunc  14808  fthfunc  14809  prfcl  15005  curf1cl  15030  curfcl  15034  hofcl  15061  odinv  16053  lsmelvalix  16131  dprdval  16473  dprdvalOLD  16475  lsp0  17067  lss0v  17074  coe1scl  17714  zndvds0  17958  frlmlbs  18200  lindfres  18227  lmisfree  18246  ntrin  18640  lpsscls  18720  restperf  18763  txuni2  19113  txopn  19150  elqtop2  19249  xkocnv  19362  ptcmp  19605  xblpnfps  19945  xblpnf  19946  bl2in  19950  unirnblps  19969  unirnbl  19970  blpnfctr  19986  dscopn  20141  bcthlem4  20813  minveclem2  20888  minveclem4  20894  icombl  21020  i1fadd  21148  i1fmul  21149  dvn1  21375  dvexp3  21425  plyconst  21649  plyid  21652  sincosq1eq  21949  sinord  21965  cxpp1  22100  cxpsqrlem  22122  cxpsqr  22123  angneg  22174  dcubic  22216  issqf  22449  ppiub  22518  bposlem1  22598  bposlem2  22599  bposlem9  22606  axlowdimlem6  23144  axlowdimlem14  23152  axcontlem2  23162  gx0  23699  gx1  23700  gxm1  23706  gxnn0add  23712  gxnn0mul  23715  ipasslem1  24182  ipasslem2  24183  ipasslem11  24191  minvecolem2  24227  minvecolem3  24228  minvecolem4  24232  shsva  24674  h1datomi  24935  lnfnmuli  25399  leopsq  25484  nmopleid  25494  opsqrlem6  25500  pjnmopi  25503  hstle  25585  csmdsymi  25689  atcvatlem  25740  elsx  26560  dya2iocnrect  26648  cvmliftphtlem  27158  wlimeq12  27707  nofulllem4  27797  fvray  28123  fvline  28126  bpoly2  28151  bpoly3  28152  fsumcube  28154  tan2h  28377  mblfinlem4  28384  mbfresfi  28391  mbfposadd  28392  dvtanlem  28394  itg2addnc  28399  ftc1anclem5  28424  ftc1anclem8  28427  dvasin  28433  tailfb  28551  heiborlem7  28669  igenidl  28816  eldioph4b  29103  diophren  29105  rmxp1  29226  rmyp1  29227  rmxm1  29228  rmym1  29229  wepwso  29348  wwlkn0s  30292  clwwlkn2  30391  rusgranumwlkb0  30524  onetansqsecsq  30985  cotsqcscsq  30986  dpfrac1  30996  atlatmstc  32804  dihglblem2N  34779