Theorem mp3an2 1297

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 1182	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
4	1, 3	mpanl2 676	1 |- ( ( ph /\ ch ) -> th )

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

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 962

This theorem is referenced by:  mp3anl2  1304  tz7.7  4741  ordin  4745  onfr  4754  tfrlem11  6843  epfrs  7947  zorng  8669  tsk2  8928  tskcard  8944  gruina  8981  muladd11  9535  00id  9540  negsub  9653  subneg  9654  muleqadd  9976  diveq1  10021  conjmul  10044  recp1lt1  10226  nnsub  10356  addltmul  10556  nnunb  10571  zltp1le  10690  gtndiv  10715  eluzp1m1  10880  zbtwnre  10947  rebtwnz  10948  supxrbnd  11287  divelunit  11423  fznatpl1  11506  flbi2  11661  fldiv  11695  modid  11728  modm1p1mod0  11746  fzen2  11787  nn0ennn  11797  seqshft2  11828  seqf1olem1  11841  ser1const  11858  sq01  11982  expnbnd  11989  faclbnd3  12064  faclbnd5  12070  hashunsng  12150  hashxplem  12191  ccatrid  12281  sgnn  12579  sqrlem2  12729  sqrlem7  12734  leabs  12784  abs2dif  12816  cvgrat  13339  cos2t  13458  sin01gt0  13470  cos01gt0  13471  demoivre  13480  demoivreALT  13481  znnenlem  13490  rpnnen2lem5  13497  rpnnen2  13504  gcd0id  13703  sqgcd  13738  isprm3  13768  eulerthlem2  13853  omeo  13877  pczpre  13910  pcrec  13921  ressress  14231  mulgm1  15639  gsumsn  16441  unitgrpid  16751  mdet0pr  18362  m2detleib  18396  cmpcov2  18952  ufileu  19451  tgpconcompeqg  19641  itg2ge0  21172  mdegldg  21496  abssinper  21939  ppiub  22502  chtub  22510  bposlem2  22583  lgs1  22636  colinearalglem4  23090  axsegconlem1  23098  axpaschlem  23121  axcontlem2  23146  axcontlem4  23148  axcontlem7  23151  axcontlem8  23152  constr2spthlem1  23428  2pthon3v  23438  vc0  23882  vcm  23884  vcnegsubdi2  23888  vcsub4  23889  nvmval2  23958  nvzs  23960  nvmf  23961  nvmdi  23965  nvnegneg  23966  nvsubadd  23970  nvpncan2  23971  nvaddsub4  23976  nvnncan  23978  nvm1  23987  nvdif  23988  nvpi  23989  nvz0  23991  nvmtri  23994  nvabs  23996  nvge0  23997  imsmetlem  24016  4ipval2  24038  ipval3  24039  ipidsq  24043  dipcj  24047  sspmval  24066  ipasslem1  24166  ipasslem2  24167  dipsubdir  24183  hvsubdistr1  24386  shsubcl  24558  shsel3  24653  shunssi  24706  hosubdi  25147  lnopmi  25339  nmophmi  25370  nmopcoi  25434  opsqrlem6  25484  hstle  25569  hst0  25572  mdsl2i  25661  superpos  25693  dmdbr5ati  25761  gsumsnf  26179  resvsca  26234  cvmliftphtlem  27136  wfrlem14  27666  finixpnum  28339  tan2h  28349  mblfinlem2  28354  mblfinlem4  28356  ismblfin  28357  elnnrabdioph  29070  rabren3dioph  29079  zindbi  29212  expgrowth  29534  trelpss  29636  el2spthonot  30314  el2spthonot0  30315  frg2woteq  30578  pgrple2abel  30685  atlatle  32687  pmaple  33127  dihglblem2N  34661