Theorem mp3an2 1352

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

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

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 987

This theorem is referenced by:  mp3anl2  1359  tz7.7  5449  ordin  5453  onfr  5462  wfrlem14  7049  wfrlem17  7052  tfrlem11  7106  epfrs  8215  zorng  8934  tsk2  9190  tskcard  9206  gruina  9243  muladd11  9803  00id  9808  negsub  9922  subneg  9923  muleqadd  10256  diveq1  10301  conjmul  10324  recp1lt1  10504  nnsub  10648  addltmul  10848  nnunb  10865  zltp1le  10986  gtndiv  11013  eluzp1m1  11182  zbtwnre  11262  rebtwnz  11263  supxrbnd  11614  divelunit  11774  fznatpl1  11850  flbi2  12052  fldiv  12087  modid  12121  modm1p1mod0  12141  fzen2  12182  nn0ennn  12192  seqshft2  12239  seqf1olem1  12252  ser1const  12269  sq01  12394  expnbnd  12401  faclbnd3  12477  faclbnd5  12483  hashunsng  12571  hashxplem  12605  ccatrid  12731  sgnn  13157  sqrlem2  13307  sqrlem7  13312  leabs  13362  abs2dif  13395  cvgrat  13939  cos2t  14232  sin01gt0  14244  cos01gt0  14245  demoivre  14254  demoivreALT  14255  znnenlem  14264  rpnnen2lem5  14271  rpnnen2  14278  gcd0id  14487  sqgcd  14526  isprm3  14633  eulerthlem2  14730  omeo  14764  pczpre  14797  pcrec  14808  ressress  15187  mulgm1  16777  unitgrpid  17897  mdet0pr  19617  m2detleib  19656  cmpcov2  20405  ufileu  20934  tgpconcompeqg  21126  itg2ge0  22693  mdegldg  23015  abssinper  23473  ppiub  24132  chtub  24140  bposlem2  24213  lgs1  24266  colinearalglem4  24939  axsegconlem1  24947  axpaschlem  24970  axcontlem2  24995  axcontlem4  24997  axcontlem7  25000  axcontlem8  25001  constr2spthlem1  25324  2pthon3v  25334  el2spthonot  25598  el2spthonot0  25599  frg2woteq  25788  vc0  26188  vcm  26190  vcnegsubdi2  26194  vcsub4  26195  nvmval2  26264  nvzs  26266  nvmf  26267  nvmdi  26271  nvnegneg  26272  nvsubadd  26276  nvpncan2  26277  nvaddsub4  26282  nvnncan  26284  nvm1  26293  nvdif  26294  nvpi  26295  nvz0  26297  nvmtri  26300  nvabs  26302  nvge0  26303  imsmetlem  26322  4ipval2  26344  ipval3  26345  ipidsq  26349  dipcj  26353  sspmval  26372  ipasslem1  26472  ipasslem2  26473  dipsubdir  26489  hvsubdistr1  26702  shsubcl  26873  shsel3  26968  shunssi  27021  hosubdi  27461  lnopmi  27653  nmophmi  27684  nmopcoi  27748  opsqrlem6  27798  hstle  27883  hst0  27886  mdsl2i  27975  superpos  28007  dmdbr5ati  28075  resvsca  28593  cvmliftphtlem  30040  topdifinffinlem  31750  finixpnum  31930  tan2h  31937  poimirlem3  31943  poimirlem4  31944  poimirlem7  31947  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem24  31964  poimirlem28  31968  mblfinlem2  31978  mblfinlem4  31980  ismblfin  31981  atlatle  32886  pmaple  33326  dihglblem2N  34862  elnnrabdioph  35650  rabren3dioph  35658  zindbi  35794  expgrowth  36684  binomcxplemnotnn0  36705  trelpss  36808  ltaddneg  37508  etransc  38149  upgredg  39228  uspgrloopnb0  39556  uspgrloopvd2  39557  01wlk  39704  0Trl  39710  pgrple2abl  40203  aacllem  40593