Theorem mp3an3 1362

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 1217	. 2 |- ( ( ph /\ ps ) -> ( ch -> th ) )
4	1, 3	mpi 20	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  mp3an13  1364  mp3an23  1365  mp3anl3  1369  opelxp  4886  ov  6448  ovmpt2a  6459  ovmpt2  6464  oaword1  7284  oneo  7313  oeoalem  7328  oeoelem  7330  nnaword1  7361  nnneo  7383  erov  7491  enrefg  7632  f1imaen  7662  mapxpen  7769  acnlem  8510  cdacomen  8642  infmap  9032  canthnumlem  9104  tskin  9215  tsksn  9216  tsk0  9219  gruxp  9263  gruina  9274  genpprecl  9457  addsrpr  9530  mulsrpr  9531  supsrlem  9566  mulid1  9671  00id  9839  mul02lem1  9840  ltneg  10147  leneg  10150  suble0  10161  div1  10332  nnaddcl  10664  nnmulcl  10665  nnge1  10668  nnsub  10681  2halves  10875  halfaddsub  10880  addltmul  10882  zleltp1  11021  nnaddm1cl  11027  zextlt  11044  eluzp1p1  11218  uzaddcl  11249  znq  11302  xrre  11498  xrre2  11499  fzshftral  11917  fraclt1  12076  expadd  12352  expmul  12355  expubnd  12371  sqmul  12376  bernneq  12436  faclbnd2  12514  faclbnd6  12522  hashgadd  12594  hashun2  12600  hashssdif  12627  hashfun  12648  ccatlcan  12871  ccatrcan  12872  shftval3  13194  sqrlem1  13361  caubnd2  13475  bpoly2  14165  bpoly3  14166  fsumcube  14168  efexp  14210  efival  14261  cos01gt0  14300  odd2np1  14420  divalglem5OLD  14431  divalglem5  14432  gcdmultiple  14573  sqgcd  14581  nn0seqcvgd  14584  phiprmpw  14779  eulerthlem2  14785  odzcllem  14792  odzcllemOLD  14798  omoe  14817  opeo  14818  pythagtriplem15  14834  pythagtriplem17  14836  pcelnn  14874  4sqlem3  14949  xpscfn  15520  fullfunc  15866  fthfunc  15867  prfcl  16143  curf1cl  16168  curfcl  16172  hofcl  16199  odinv  17267  lsmelvalix  17348  dprdval  17690  lsp0  18287  lss0v  18294  coe1scl  18935  zndvds0  19176  frlmlbs  19410  lindfres  19436  lmisfree  19455  ntrin  20131  lpsscls  20212  restperf  20255  txuni2  20635  txopn  20672  elqtop2  20771  xkocnv  20884  ptcmp  21128  xblpnfps  21465  xblpnf  21466  bl2in  21470  unirnblps  21489  unirnbl  21490  blpnfctr  21506  dscopn  21643  bcthlem4  22350  minveclem2  22423  minveclem4  22429  minveclem2OLD  22435  minveclem4OLD  22441  icombl  22573  i1fadd  22709  i1fmul  22710  dvn1  22936  dvexp3  22986  plyconst  23216  plyid  23219  sincosq1eq  23523  sinord  23539  cxpp1  23681  cxpsqrtlem  23703  cxpsqrt  23704  angneg  23788  dcubic  23828  issqf  24119  ppiub  24188  bposlem1  24268  bposlem2  24269  bposlem9  24276  axlowdimlem6  25033  axlowdimlem14  25041  axcontlem2  25051  wwlkn0s  25489  clwwlkn2  25559  rusgranumwlkb0  25737  gx0  26045  gx1  26046  gxm1  26052  gxnn0add  26058  gxnn0mul  26061  ipasslem1  26528  ipasslem2  26529  ipasslem11  26537  minvecolem2  26573  minvecolem3  26574  minvecolem4  26578  minvecolem2OLD  26583  minvecolem3OLD  26584  minvecolem4OLD  26588  shsva  27029  h1datomi  27290  lnfnmuli  27753  leopsq  27838  nmopleid  27848  opsqrlem6  27854  pjnmopi  27857  hstle  27939  csmdsymi  28043  atcvatlem  28094  elsx  29067  dya2iocnrect  29153  cvmliftphtlem  30090  wlimeq12  30552  nofulllem4  30644  fvray  30958  fvline  30961  tailfb  31083  tan2h  31983  poimirlem32  32018  mblfinlem4  32026  mbfresfi  32033  mbfposadd  32034  dvtanlemOLD  32037  itg2addnc  32042  ftc1anclem5  32067  ftc1anclem8  32070  dvasin  32074  heiborlem7  32195  igenidl  32342  atlatmstc  32931  dihglblem2N  34908  eldioph4b  35700  diophren  35702  rmxp1  35826  rmyp1  35827  rmxm1  35828  rmym1  35829  wepwso  35947  pfx2  39090  structgrssvtxlem  39267  pthdlem2  39890  0ewlk  39924  dig0  40786  onetansqsecsq  40850  cotsqcscsq  40851  dpfrac1  40861