Theorem mp3an2 1310

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 1194	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 679	1 |- ( ( ph /\ ch ) -> 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:  mp3anl2  1317  tz7.7  4893  ordin  4897  onfr  4906  tfrlem11  7049  epfrs  8153  zorng  8875  tsk2  9132  tskcard  9148  gruina  9185  muladd11  9739  00id  9744  negsub  9858  subneg  9859  muleqadd  10189  diveq1  10234  conjmul  10257  recp1lt1  10438  nnsub  10570  addltmul  10770  nnunb  10787  zltp1le  10909  gtndiv  10936  eluzp1m1  11105  zbtwnre  11181  rebtwnz  11182  supxrbnd  11523  divelunit  11665  fznatpl1  11738  flbi2  11934  fldiv  11969  modid  12002  modm1p1mod0  12020  fzen2  12061  nn0ennn  12071  seqshft2  12115  seqf1olem1  12128  ser1const  12145  sq01  12270  expnbnd  12277  faclbnd3  12352  faclbnd5  12358  hashunsng  12443  hashxplem  12475  ccatrid  12593  sgnn  13009  sqrlem2  13159  sqrlem7  13164  leabs  13214  abs2dif  13247  cvgrat  13774  cos2t  13995  sin01gt0  14007  cos01gt0  14008  demoivre  14017  demoivreALT  14018  znnenlem  14029  rpnnen2lem5  14036  rpnnen2  14043  gcd0id  14245  sqgcd  14280  isprm3  14310  eulerthlem2  14396  omeo  14422  pczpre  14455  pcrec  14466  ressress  14781  mulgm1  16360  unitgrpid  17513  mdet0pr  19261  m2detleib  19300  cmpcov2  20057  ufileu  20586  tgpconcompeqg  20776  itg2ge0  22308  mdegldg  22632  abssinper  23077  ppiub  23677  chtub  23685  bposlem2  23758  lgs1  23811  colinearalglem4  24414  axsegconlem1  24422  axpaschlem  24445  axcontlem2  24470  axcontlem4  24472  axcontlem7  24475  axcontlem8  24476  constr2spthlem1  24798  2pthon3v  24808  el2spthonot  25072  el2spthonot0  25073  frg2woteq  25262  vc0  25660  vcm  25662  vcnegsubdi2  25666  vcsub4  25667  nvmval2  25736  nvzs  25738  nvmf  25739  nvmdi  25743  nvnegneg  25744  nvsubadd  25748  nvpncan2  25749  nvaddsub4  25754  nvnncan  25756  nvm1  25765  nvdif  25766  nvpi  25767  nvz0  25769  nvmtri  25772  nvabs  25774  nvge0  25775  imsmetlem  25794  4ipval2  25816  ipval3  25817  ipidsq  25821  dipcj  25825  sspmval  25844  ipasslem1  25944  ipasslem2  25945  dipsubdir  25961  hvsubdistr1  26164  shsubcl  26336  shsel3  26431  shunssi  26484  hosubdi  26925  lnopmi  27117  nmophmi  27148  nmopcoi  27212  opsqrlem6  27262  hstle  27347  hst0  27350  mdsl2i  27439  superpos  27471  dmdbr5ati  27539  resvsca  28055  cvmliftphtlem  29026  wfrlem14  29596  finixpnum  30278  tan2h  30287  mblfinlem2  30292  mblfinlem4  30294  ismblfin  30295  elnnrabdioph  30980  rabren3dioph  30988  zindbi  31121  expgrowth  31481  binomcxplemnotnn0  31502  trelpss  31605  ltaddneg  31724  etransc  32305  pgrple2abl  33212  aacllem  33604  atlatle  35442  pmaple  35882  dihglblem2N  37418