Theorem mp3an2 1307

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

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

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 970

This theorem is referenced by:  mp3anl2  1314  tz7.7  4897  ordin  4901  onfr  4910  tfrlem11  7047  epfrs  8151  zorng  8873  tsk2  9132  tskcard  9148  gruina  9185  muladd11  9738  00id  9743  negsub  9856  subneg  9857  muleqadd  10182  diveq1  10227  conjmul  10250  recp1lt1  10432  nnsub  10563  addltmul  10763  nnunb  10780  zltp1le  10901  gtndiv  10927  eluzp1m1  11094  zbtwnre  11169  rebtwnz  11170  supxrbnd  11509  divelunit  11651  fznatpl1  11723  flbi2  11909  fldiv  11943  modid  11976  modm1p1mod0  11994  fzen2  12035  nn0ennn  12045  seqshft2  12089  seqf1olem1  12102  ser1const  12119  sq01  12243  expnbnd  12250  faclbnd3  12325  faclbnd5  12331  hashunsng  12414  hashxplem  12444  ccatrid  12556  sgnn  12877  sqrlem2  13027  sqrlem7  13032  leabs  13082  abs2dif  13114  cvgrat  13644  cos2t  13763  sin01gt0  13775  cos01gt0  13776  demoivre  13785  demoivreALT  13786  znnenlem  13795  rpnnen2lem5  13802  rpnnen2  13809  gcd0id  14009  sqgcd  14044  isprm3  14074  eulerthlem2  14160  omeo  14186  pczpre  14219  pcrec  14230  ressress  14541  mulgm1  15954  unitgrpid  17095  mdet0pr  18854  m2detleib  18893  cmpcov2  19649  ufileu  20148  tgpconcompeqg  20338  itg2ge0  21870  mdegldg  22194  abssinper  22637  ppiub  23200  chtub  23208  bposlem2  23281  lgs1  23334  colinearalglem4  23881  axsegconlem1  23889  axpaschlem  23912  axcontlem2  23937  axcontlem4  23939  axcontlem7  23942  axcontlem8  23943  constr2spthlem1  24258  2pthon3v  24268  el2spthonot  24532  el2spthonot0  24533  frg2woteq  24723  vc0  25124  vcm  25126  vcnegsubdi2  25130  vcsub4  25131  nvmval2  25200  nvzs  25202  nvmf  25203  nvmdi  25207  nvnegneg  25208  nvsubadd  25212  nvpncan2  25213  nvaddsub4  25218  nvnncan  25220  nvm1  25229  nvdif  25230  nvpi  25231  nvz0  25233  nvmtri  25236  nvabs  25238  nvge0  25239  imsmetlem  25258  4ipval2  25280  ipval3  25281  ipidsq  25285  dipcj  25289  sspmval  25308  ipasslem1  25408  ipasslem2  25409  dipsubdir  25425  hvsubdistr1  25628  shsubcl  25800  shsel3  25895  shunssi  25948  hosubdi  26389  lnopmi  26581  nmophmi  26612  nmopcoi  26676  opsqrlem6  26726  hstle  26811  hst0  26814  mdsl2i  26903  superpos  26935  dmdbr5ati  27003  resvsca  27469  cvmliftphtlem  28388  wfrlem14  28919  finixpnum  29601  tan2h  29611  mblfinlem2  29616  mblfinlem4  29618  ismblfin  29619  elnnrabdioph  30331  rabren3dioph  30340  zindbi  30473  expgrowth  30795  trelpss  30897  ltaddneg  31016  pgrple2abl  31898  atlatle  33992  pmaple  34432  dihglblem2N  35966