Theorem mp3an2 1349

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	|- ps
mp3an2.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an2	|- ( ( ph /\ ch ) -> th )

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 |- ps
2		mp3an2.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expa 1206	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 686	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 983

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 189  df-an 373  df-3an 985

This theorem is referenced by:  mp3anl2  1356  tz7.7  5466  ordin  5470  onfr  5479  wfrlem14  7055  wfrlem17  7058  tfrlem11  7112  epfrs  8218  zorng  8936  tsk2  9192  tskcard  9208  gruina  9245  muladd11  9805  00id  9810  negsub  9924  subneg  9925  muleqadd  10258  diveq1  10303  conjmul  10326  recp1lt1  10506  nnsub  10650  addltmul  10850  nnunb  10867  zltp1le  10988  gtndiv  11015  eluzp1m1  11184  zbtwnre  11264  rebtwnz  11265  supxrbnd  11616  divelunit  11776  fznatpl1  11852  flbi2  12053  fldiv  12088  modid  12122  modm1p1mod0  12142  fzen2  12183  nn0ennn  12193  seqshft2  12240  seqf1olem1  12253  ser1const  12270  sq01  12395  expnbnd  12402  faclbnd3  12478  faclbnd5  12484  hashunsng  12572  hashxplem  12604  ccatrid  12729  sgnn  13151  sqrlem2  13301  sqrlem7  13306  leabs  13356  abs2dif  13389  cvgrat  13932  cos2t  14225  sin01gt0  14237  cos01gt0  14238  demoivre  14247  demoivreALT  14248  znnenlem  14257  rpnnen2lem5  14264  rpnnen2  14271  gcd0id  14480  sqgcd  14519  isprm3  14626  eulerthlem2  14723  omeo  14757  pczpre  14790  pcrec  14801  ressress  15180  mulgm1  16770  unitgrpid  17890  mdet0pr  19609  m2detleib  19648  cmpcov2  20397  ufileu  20926  tgpconcompeqg  21118  itg2ge0  22685  mdegldg  23007  abssinper  23465  ppiub  24124  chtub  24132  bposlem2  24205  lgs1  24258  colinearalglem4  24931  axsegconlem1  24939  axpaschlem  24962  axcontlem2  24987  axcontlem4  24989  axcontlem7  24992  axcontlem8  24993  constr2spthlem1  25316  2pthon3v  25326  el2spthonot  25590  el2spthonot0  25591  frg2woteq  25780  vc0  26180  vcm  26182  vcnegsubdi2  26186  vcsub4  26187  nvmval2  26256  nvzs  26258  nvmf  26259  nvmdi  26263  nvnegneg  26264  nvsubadd  26268  nvpncan2  26269  nvaddsub4  26274  nvnncan  26276  nvm1  26285  nvdif  26286  nvpi  26287  nvz0  26289  nvmtri  26292  nvabs  26294  nvge0  26295  imsmetlem  26314  4ipval2  26336  ipval3  26337  ipidsq  26341  dipcj  26345  sspmval  26364  ipasslem1  26464  ipasslem2  26465  dipsubdir  26481  hvsubdistr1  26694  shsubcl  26865  shsel3  26960  shunssi  27013  hosubdi  27453  lnopmi  27645  nmophmi  27676  nmopcoi  27740  opsqrlem6  27790  hstle  27875  hst0  27878  mdsl2i  27967  superpos  27999  dmdbr5ati  28067  resvsca  28595  cvmliftphtlem  30042  topdifinffinlem  31708  finixpnum  31888  tan2h  31895  poimirlem3  31901  poimirlem4  31902  poimirlem7  31905  poimirlem16  31914  poimirlem17  31915  poimirlem19  31917  poimirlem20  31918  poimirlem24  31922  poimirlem28  31926  mblfinlem2  31936  mblfinlem4  31938  ismblfin  31939  atlatle  32849  pmaple  33289  dihglblem2N  34825  elnnrabdioph  35613  rabren3dioph  35621  zindbi  35758  expgrowth  36586  binomcxplemnotnn0  36607  trelpss  36710  ltaddneg  37394  etransc  38013  pgrple2abl  39494  aacllem  39884