Theorem mp3an2 1302

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 1187	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 681	1 |- ( ( ph /\ ch ) -> 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:  mp3anl2  1309  tz7.7  4748  ordin  4752  onfr  4761  tfrlem11  6850  epfrs  7954  zorng  8676  tsk2  8935  tskcard  8951  gruina  8988  muladd11  9542  00id  9547  negsub  9660  subneg  9661  muleqadd  9983  diveq1  10028  conjmul  10051  recp1lt1  10233  nnsub  10363  addltmul  10563  nnunb  10578  zltp1le  10697  gtndiv  10722  eluzp1m1  10887  zbtwnre  10954  rebtwnz  10955  supxrbnd  11294  divelunit  11430  fznatpl1  11513  flbi2  11668  fldiv  11702  modid  11735  modm1p1mod0  11753  fzen2  11794  nn0ennn  11804  seqshft2  11835  seqf1olem1  11848  ser1const  11865  sq01  11989  expnbnd  11996  faclbnd3  12071  faclbnd5  12077  hashunsng  12157  hashxplem  12198  ccatrid  12288  sgnn  12586  sqrlem2  12736  sqrlem7  12741  leabs  12791  abs2dif  12823  cvgrat  13346  cos2t  13465  sin01gt0  13477  cos01gt0  13478  demoivre  13487  demoivreALT  13488  znnenlem  13497  rpnnen2lem5  13504  rpnnen2  13511  gcd0id  13710  sqgcd  13745  isprm3  13775  eulerthlem2  13860  omeo  13884  pczpre  13917  pcrec  13928  ressress  14238  mulgm1  15649  gsumsn  16452  unitgrpid  16764  mdet0pr  18406  m2detleib  18440  cmpcov2  18996  ufileu  19495  tgpconcompeqg  19685  itg2ge0  21216  mdegldg  21540  abssinper  21983  ppiub  22546  chtub  22554  bposlem2  22627  lgs1  22680  colinearalglem4  23158  axsegconlem1  23166  axpaschlem  23189  axcontlem2  23214  axcontlem4  23216  axcontlem7  23219  axcontlem8  23220  constr2spthlem1  23496  2pthon3v  23506  vc0  23950  vcm  23952  vcnegsubdi2  23956  vcsub4  23957  nvmval2  24026  nvzs  24028  nvmf  24029  nvmdi  24033  nvnegneg  24034  nvsubadd  24038  nvpncan2  24039  nvaddsub4  24044  nvnncan  24046  nvm1  24055  nvdif  24056  nvpi  24057  nvz0  24059  nvmtri  24062  nvabs  24064  nvge0  24065  imsmetlem  24084  4ipval2  24106  ipval3  24107  ipidsq  24111  dipcj  24115  sspmval  24134  ipasslem1  24234  ipasslem2  24235  dipsubdir  24251  hvsubdistr1  24454  shsubcl  24626  shsel3  24721  shunssi  24774  hosubdi  25215  lnopmi  25407  nmophmi  25438  nmopcoi  25502  opsqrlem6  25552  hstle  25637  hst0  25640  mdsl2i  25729  superpos  25761  dmdbr5ati  25829  gsumsnf  26247  resvsca  26301  cvmliftphtlem  27209  wfrlem14  27740  finixpnum  28417  tan2h  28427  mblfinlem2  28432  mblfinlem4  28434  ismblfin  28435  elnnrabdioph  29148  rabren3dioph  29157  zindbi  29290  expgrowth  29612  trelpss  29714  el2spthonot  30392  el2spthonot0  30393  frg2woteq  30656  pgrple2abel  30771  atlatle  32968  pmaple  33408  dihglblem2N  34942