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

Theorem mp3an3 1312
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 1197 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 17 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 974
This theorem is referenced by:  mp3an13  1314  mp3an23  1315  mp3anl3  1319  opelxp  5016  ov  6404  ovmpt2a  6415  ovmpt2  6420  oaword1  7200  oneo  7229  oeoalem  7244  oeoelem  7246  nnaword1  7277  nnneo  7299  erov  7407  enrefg  7546  f1imaen  7576  mapxpen  7682  acnlem  8429  cdacomen  8561  infmap  8951  canthnumlem  9026  tskin  9137  tsksn  9138  tsk0  9141  gruxp  9185  gruina  9196  genpprecl  9379  addsrpr  9452  mulsrpr  9453  supsrlem  9488  mulid1  9593  00id  9755  mul02lem1  9756  ltneg  10055  leneg  10058  suble0  10069  div1  10239  nnaddcl  10561  nnmulcl  10562  nnge1  10565  nnsub  10577  2halves  10770  halfaddsub  10775  addltmul  10777  zleltp1  10917  nnaddm1cl  10923  zextlt  10940  uzindOLD  10960  eluzp1p1  11112  uzaddcl  11143  znq  11192  xrre  11376  xrre2  11377  fzshftral  11771  fraclt1  11915  expadd  12184  expmul  12187  expubnd  12202  sqmul  12207  bernneq  12268  faclbnd2  12345  faclbnd6  12353  hashgadd  12421  hashun2  12427  hashssdif  12451  hashfun  12471  ccatlcan  12673  ccatrcan  12674  shftval3  12885  sqrlem1  13052  caubnd2  13166  efexp  13710  efival  13761  cos01gt0  13800  odd2np1  13920  divalglem5  13929  gcdmultiple  14062  sqgcd  14070  nn0seqcvgd  14073  phiprmpw  14180  eulerthlem2  14186  odzcllem  14193  omoe  14210  opeo  14211  pythagtriplem15  14227  pythagtriplem17  14229  pcelnn  14267  4sqlem3  14342  xpscfn  14830  fullfunc  15146  fthfunc  15147  prfcl  15343  curf1cl  15368  curfcl  15372  hofcl  15399  odinv  16454  lsmelvalix  16532  dprdval  16905  dprdvalOLD  16907  lsp0  17526  lss0v  17533  coe1scl  18199  zndvds0  18459  frlmlbs  18701  lindfres  18728  lmisfree  18747  ntrin  19432  lpsscls  19512  restperf  19555  txuni2  19936  txopn  19973  elqtop2  20072  xkocnv  20185  ptcmp  20428  xblpnfps  20768  xblpnf  20769  bl2in  20773  unirnblps  20792  unirnbl  20793  blpnfctr  20809  dscopn  20964  bcthlem4  21636  minveclem2  21711  minveclem4  21717  icombl  21844  i1fadd  21972  i1fmul  21973  dvn1  22199  dvexp3  22249  plyconst  22473  plyid  22476  sincosq1eq  22774  sinord  22790  cxpp1  22930  cxpsqrtlem  22952  cxpsqrt  22953  angneg  23004  dcubic  23046  issqf  23279  ppiub  23348  bposlem1  23428  bposlem2  23429  bposlem9  23436  axlowdimlem6  24119  axlowdimlem14  24127  axcontlem2  24137  wwlkn0s  24574  clwwlkn2  24644  rusgranumwlkb0  24822  gx0  25132  gx1  25133  gxm1  25139  gxnn0add  25145  gxnn0mul  25148  ipasslem1  25615  ipasslem2  25616  ipasslem11  25624  minvecolem2  25660  minvecolem3  25661  minvecolem4  25665  shsva  26107  h1datomi  26368  lnfnmuli  26832  leopsq  26917  nmopleid  26927  opsqrlem6  26933  pjnmopi  26936  hstle  27018  csmdsymi  27122  atcvatlem  27173  elsx  28035  dya2iocnrect  28122  cvmliftphtlem  28632  wlimeq12  29347  nofulllem4  29437  fvray  29763  fvline  29766  bpoly2  29791  bpoly3  29792  fsumcube  29794  tan2h  30019  mblfinlem4  30026  mbfresfi  30033  mbfposadd  30034  dvtanlem  30036  itg2addnc  30041  ftc1anclem5  30066  ftc1anclem8  30069  dvasin  30075  tailfb  30167  heiborlem7  30285  igenidl  30432  eldioph4b  30717  diophren  30719  rmxp1  30840  rmyp1  30841  rmxm1  30842  rmym1  30843  wepwso  30960  onetansqsecsq  32885  cotsqcscsq  32886  dpfrac1  32896  atlatmstc  34767  dihglblem2N  36744
  Copyright terms: Public domain W3C validator