MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an3 Structured version   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  4908  ov  6193  ovmpt2a  6204  ovmpt2  6209  oaword1  6795  oneo  6824  oeoalem  6839  oeoelem  6841  nnaword1  6872  nnneo  6894  erov  7001  th3q  7013  enrefg  7139  f1imaen  7169  mapxpen  7273  acnlem  7929  cdacomen  8061  infmap  8451  canthnumlem  8523  tskin  8634  tsksn  8635  tsk0  8638  gruxp  8682  gruina  8693  genpprecl  8878  supsrlem  8986  mulid1  9088  00id  9241  mul02lem1  9242  ltneg  9528  leneg  9531  suble0  9542  div1  9707  nnaddcl  10022  nnmulcl  10023  nnge1  10026  nnsub  10038  2halves  10196  halfaddsub  10201  addltmul  10203  zleltp1  10326  nnaddm1cl  10331  zextlt  10344  uzindOLD  10364  eluzp1p1  10511  uzaddcl  10533  znq  10578  xrre  10757  xrre2  10758  fzshftral  11134  fraclt1  11211  expadd  11422  expmul  11425  expubnd  11440  sqmul  11445  bernneq  11505  faclbnd2  11582  faclbnd6  11590  hashgadd  11651  hashun2  11657  hashssdif  11677  hashfun  11700  ccatlcan  11778  ccatrcan  11779  shftval3  11891  sqrlem1  12048  caubnd2  12161  efexp  12702  efival  12753  cos01gt0  12792  odd2np1  12908  divalglem5  12917  gcdmultiple  13050  sqgcd  13058  nn0seqcvgd  13061  phiprmpw  13165  eulerthlem2  13171  odzcllem  13178  omoe  13186  opeo  13187  pythagtriplem15  13203  pythagtriplem17  13205  pcelnn  13243  4sqlem3  13318  xpscfn  13784  fullfunc  14103  fthfunc  14104  prfcl  14300  curf1cl  14325  curfcl  14329  hofcl  14356  odinv  15197  lsmelvalix  15275  dprdval  15561  lsp0  16085  lss0v  16092  coe1scl  16678  zndvds0  16831  ntrin  17125  lpsscls  17205  restperf  17248  txuni2  17597  txopn  17634  elqtop2  17733  xkocnv  17846  ptcmp  18089  xblpnfps  18425  xblpnf  18426  bl2in  18430  unirnblps  18449  unirnbl  18450  blpnfctr  18466  dscopn  18621  bcthlem4  19280  minveclem2  19327  minveclem4  19333  icombl  19458  i1fadd  19587  i1fmul  19588  dvn1  19812  dvexp3  19862  plyconst  20125  plyid  20128  sincosq1eq  20420  sinord  20436  cxpp1  20571  cxpsqrlem  20593  cxpsqr  20594  angneg  20645  dcubic  20686  issqf  20919  ppiub  20988  bposlem1  21068  bposlem2  21069  bposlem9  21076  gx0  21849  gx1  21850  gxm1  21856  gxnn0add  21862  gxnn0mul  21865  ipasslem1  22332  ipasslem2  22333  ipasslem11  22341  minvecolem2  22377  minvecolem3  22378  minvecolem4  22382  shsva  22822  h1datomi  23083  lnfnmuli  23547  leopsq  23632  nmopleid  23642  opsqrlem6  23648  pjnmopi  23651  hstle  23733  csmdsymi  23837  atcvatlem  23888  elsx  24548  dya2iocnrect  24631  sibfof  24654  cvmliftphtlem  25004  wlimeq12  25570  nofulllem4  25660  axlowdimlem6  25886  axlowdimlem14  25894  axcontlem2  25904  fvray  26075  fvline  26078  bpoly2  26103  bpoly3  26104  fsumcube  26106  mblfinlem4  26246  mbfresfi  26253  mbfposadd  26254  itg2addnc  26259  ftc1anclem5  26284  ftc1anclem8  26287  tailfb  26406  heiborlem7  26526  igenidl  26673  eldioph4b  26872  diophren  26874  rmxp1  26995  rmyp1  26996  rmxm1  26997  rmym1  26998  wepwso  27117  frlmlbs  27226  lindfres  27270  lmisfree  27289  onetansqsecsq  28504  cotsqcscsq  28505  dpfrac1  28515  atlatmstc  30117  dihglblem2N  32092
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