Theorem mp3an3 1349

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	|- ch
mp3an3.2	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an3	|- ( ( ph /\ ps ) -> th )

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 |- ch
2		mp3an3.2	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
3	2	3expia 1207	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 20	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  mp3an13  1351  mp3an23  1352  mp3anl3  1356  opelxp  4883  ov  6430  ovmpt2a  6441  ovmpt2  6446  oaword1  7264  oneo  7293  oeoalem  7308  oeoelem  7310  nnaword1  7341  nnneo  7363  erov  7471  enrefg  7611  f1imaen  7641  mapxpen  7747  acnlem  8486  cdacomen  8618  infmap  9008  canthnumlem  9080  tskin  9191  tsksn  9192  tsk0  9195  gruxp  9239  gruina  9250  genpprecl  9433  addsrpr  9506  mulsrpr  9507  supsrlem  9542  mulid1  9647  00id  9815  mul02lem1  9816  ltneg  10121  leneg  10124  suble0  10135  div1  10306  nnaddcl  10638  nnmulcl  10639  nnge1  10642  nnsub  10655  2halves  10848  halfaddsub  10853  addltmul  10855  zleltp1  10994  nnaddm1cl  11000  zextlt  11017  eluzp1p1  11191  uzaddcl  11222  znq  11275  xrre  11471  xrre2  11472  fzshftral  11889  fraclt1  12044  expadd  12320  expmul  12323  expubnd  12339  sqmul  12344  bernneq  12404  faclbnd2  12482  faclbnd6  12490  hashgadd  12562  hashun2  12568  hashssdif  12593  hashfun  12613  ccatlcan  12830  ccatrcan  12831  shftval3  13139  sqrlem1  13306  caubnd2  13420  bpoly2  14109  bpoly3  14110  fsumcube  14112  efexp  14154  efival  14205  cos01gt0  14244  odd2np1  14364  divalglem5OLD  14375  divalglem5  14376  gcdmultiple  14517  sqgcd  14525  nn0seqcvgd  14528  phiprmpw  14723  eulerthlem2  14729  odzcllem  14736  odzcllemOLD  14742  omoe  14761  opeo  14762  pythagtriplem15  14778  pythagtriplem17  14780  pcelnn  14818  4sqlem3  14893  xpscfn  15464  fullfunc  15810  fthfunc  15811  prfcl  16087  curf1cl  16112  curfcl  16116  hofcl  16143  odinv  17211  lsmelvalix  17292  dprdval  17634  lsp0  18231  lss0v  18238  coe1scl  18879  zndvds0  19119  frlmlbs  19353  lindfres  19379  lmisfree  19398  ntrin  20074  lpsscls  20155  restperf  20198  txuni2  20578  txopn  20615  elqtop2  20714  xkocnv  20827  ptcmp  21071  xblpnfps  21408  xblpnf  21409  bl2in  21413  unirnblps  21432  unirnbl  21433  blpnfctr  21449  dscopn  21586  bcthlem4  22293  minveclem2  22366  minveclem4  22372  minveclem2OLD  22378  minveclem4OLD  22384  icombl  22515  i1fadd  22651  i1fmul  22652  dvn1  22878  dvexp3  22928  plyconst  23158  plyid  23161  sincosq1eq  23465  sinord  23481  cxpp1  23623  cxpsqrtlem  23645  cxpsqrt  23646  angneg  23730  dcubic  23770  issqf  24061  ppiub  24130  bposlem1  24210  bposlem2  24211  bposlem9  24218  axlowdimlem6  24975  axlowdimlem14  24983  axcontlem2  24993  wwlkn0s  25431  clwwlkn2  25501  rusgranumwlkb0  25679  gx0  25987  gx1  25988  gxm1  25994  gxnn0add  26000  gxnn0mul  26003  ipasslem1  26470  ipasslem2  26471  ipasslem11  26479  minvecolem2  26515  minvecolem3  26516  minvecolem4  26520  minvecolem2OLD  26525  minvecolem3OLD  26526  minvecolem4OLD  26530  shsva  26971  h1datomi  27232  lnfnmuli  27695  leopsq  27780  nmopleid  27790  opsqrlem6  27796  pjnmopi  27799  hstle  27881  csmdsymi  27985  atcvatlem  28036  elsx  29024  dya2iocnrect  29111  cvmliftphtlem  30048  wlimeq12  30509  nofulllem4  30599  fvray  30913  fvline  30916  tailfb  31038  tan2h  31901  poimirlem32  31936  mblfinlem4  31944  mbfresfi  31951  mbfposadd  31952  dvtanlemOLD  31955  itg2addnc  31960  ftc1anclem5  31985  ftc1anclem8  31988  dvasin  31992  heiborlem7  32113  igenidl  32260  atlatmstc  32854  dihglblem2N  34831  eldioph4b  35623  diophren  35625  rmxp1  35750  rmyp1  35751  rmxm1  35752  rmym1  35753  wepwso  35871  pfx2  38823  struct1vtxvallem  38955  dig0  40038  onetansqsecsq  40102  cotsqcscsq  40103  dpfrac1  40113