MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an3 Unicode version

Theorem mp3an3 1268
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
StepHypRef Expression
1 mp3an3.1 . 2  |-  ch
2 mp3an3.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expia 1155 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 17 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mp3an13  1270  mp3an23  1271  mp3anl3  1275  opelxp  4875  ov  6160  ovmpt2a  6171  ovmpt2  6176  oaword1  6762  oneo  6791  oeoalem  6806  oeoelem  6808  nnaword1  6839  nnneo  6861  erov  6968  th3q  6980  enrefg  7106  f1imaen  7136  mapxpen  7240  acnlem  7893  cdacomen  8025  infmap  8415  canthnumlem  8487  tskin  8598  tsksn  8599  tsk0  8602  gruxp  8646  gruina  8657  genpprecl  8842  supsrlem  8950  mulid1  9052  00id  9205  mul02lem1  9206  ltneg  9492  leneg  9495  suble0  9506  div1  9671  nnaddcl  9986  nnmulcl  9987  nnge1  9990  nnsub  10002  2halves  10160  halfaddsub  10165  addltmul  10167  zleltp1  10290  nnaddm1cl  10295  zextlt  10308  uzindOLD  10328  eluzp1p1  10475  uzaddcl  10497  znq  10542  xrre  10721  xrre2  10722  fzshftral  11097  fraclt1  11174  expadd  11385  expmul  11388  expubnd  11403  sqmul  11408  bernneq  11468  faclbnd2  11545  faclbnd6  11553  hashgadd  11614  hashun2  11620  hashssdif  11640  hashfun  11663  ccatlcan  11741  ccatrcan  11742  shftval3  11854  sqrlem1  12011  caubnd2  12124  efexp  12665  efival  12716  cos01gt0  12755  odd2np1  12871  divalglem5  12880  gcdmultiple  13013  sqgcd  13021  nn0seqcvgd  13024  phiprmpw  13128  eulerthlem2  13134  odzcllem  13141  omoe  13149  opeo  13150  pythagtriplem15  13166  pythagtriplem17  13168  pcelnn  13206  4sqlem3  13281  xpscfn  13747  fullfunc  14066  fthfunc  14067  prfcl  14263  curf1cl  14288  curfcl  14292  hofcl  14319  odinv  15160  lsmelvalix  15238  dprdval  15524  lsp0  16048  lss0v  16055  coe1scl  16641  zndvds0  16794  ntrin  17088  lpsscls  17168  restperf  17210  txuni2  17558  txopn  17595  elqtop2  17694  xkocnv  17807  ptcmp  18050  xblpnfps  18386  xblpnf  18387  bl2in  18391  unirnblps  18410  unirnbl  18411  blpnfctr  18427  dscopn  18582  bcthlem4  19241  minveclem2  19288  minveclem4  19294  icombl  19419  i1fadd  19548  i1fmul  19549  dvn1  19773  dvexp3  19823  plyconst  20086  plyid  20089  sincosq1eq  20381  sinord  20397  cxpp1  20532  cxpsqrlem  20554  cxpsqr  20555  angneg  20606  dcubic  20647  issqf  20880  ppiub  20949  bposlem1  21029  bposlem2  21030  bposlem9  21037  gx0  21810  gx1  21811  gxm1  21817  gxnn0add  21823  gxnn0mul  21826  ipasslem1  22293  ipasslem2  22294  ipasslem11  22302  minvecolem2  22338  minvecolem3  22339  minvecolem4  22343  shsva  22783  h1datomi  23044  lnfnmuli  23508  leopsq  23593  nmopleid  23603  opsqrlem6  23609  pjnmopi  23612  hstle  23694  csmdsymi  23798  atcvatlem  23849  elsx  24509  dya2iocnrect  24592  sibfof  24615  cvmliftphtlem  24965  nofulllem4  25581  axlowdimlem6  25798  axlowdimlem14  25806  axcontlem2  25816  fvray  25987  fvline  25990  bpoly2  26015  bpoly3  26016  fsumcube  26018  mblfinlem3  26153  mbfresfi  26160  mbfposadd  26161  itg2addnc  26166  tailfb  26304  heiborlem7  26424  igenidl  26571  eldioph4b  26770  diophren  26772  rmxp1  26893  rmyp1  26894  rmxm1  26895  rmym1  26896  wepwso  27015  frlmlbs  27125  lindfres  27169  lmisfree  27188  onetansqsecsq  28226  cotsqcscsq  28227  dpfrac1  28237  atlatmstc  29814  dihglblem2N  31789
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator