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

Theorem mp3an3 1266
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 1153 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
41, 3mpi 16 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mp3an13  1268  mp3an23  1269  mp3anl3  1273  opelxp  4719  ov  5967  ovmpt2a  5978  ovmpt2  5983  oaword1  6550  oneo  6579  oeoalem  6594  oeoelem  6596  nnaword1  6627  nnneo  6649  erov  6755  th3q  6767  enrefg  6893  f1imaen  6923  mapxpen  7027  acnlem  7675  cdacomen  7807  infmap  8198  canthnumlem  8270  tskin  8381  tsksn  8382  tsk0  8385  gruxp  8429  gruina  8440  genpprecl  8625  supsrlem  8733  mulid1  8835  00id  8987  mul02lem1  8988  ltneg  9274  leneg  9277  suble0  9288  div1  9453  nnaddcl  9768  nnmulcl  9769  nnge1  9772  nnsub  9784  2halves  9940  halfaddsub  9945  addltmul  9947  zleltp1  10068  nnaddm1cl  10073  zextlt  10086  uzindOLD  10106  eluzp1p1  10253  uzaddcl  10275  znq  10320  xrre  10498  xrre2  10499  fzshftral  10869  fraclt1  10934  expadd  11144  expmul  11147  expubnd  11162  sqmul  11167  bernneq  11227  faclbnd2  11304  faclbnd6  11312  hashgadd  11359  hashun2  11365  hashssdif  11374  hashfun  11389  ccatlcan  11464  ccatrcan  11465  shftval3  11571  sqrlem1  11728  caubnd2  11841  efexp  12381  efival  12432  cos01gt0  12471  odd2np1  12587  divalglem5  12596  gcdmultiple  12729  sqgcd  12737  nn0seqcvgd  12740  phiprmpw  12844  eulerthlem2  12850  odzcllem  12857  omoe  12865  opeo  12866  pythagtriplem15  12882  pythagtriplem17  12884  pcelnn  12922  4sqlem3  12997  xpscfn  13461  fullfunc  13780  fthfunc  13781  prfcl  13977  curf1cl  14002  curfcl  14006  hofcl  14033  odinv  14874  lsmelvalix  14952  dprdval  15238  lsp0  15766  lss0v  15773  coe1scl  16362  zndvds0  16504  ntrin  16798  lpsscls  16873  restperf  16914  txuni2  17260  txopn  17297  elqtop2  17392  xkocnv  17505  ptcmp  17752  xblpnf  17953  bl2in  17957  unirnbl  17969  blpnfctr  17982  dscopn  18096  bcthlem4  18749  minveclem2  18790  minveclem4  18796  icombl  18921  i1fadd  19050  i1fmul  19051  dvn1  19275  dvexp3  19325  plyconst  19588  plyid  19591  sincosq1eq  19880  sinord  19896  cxpp1  20027  cxpsqrlem  20049  cxpsqr  20050  angneg  20101  dcubic  20142  issqf  20374  ppiub  20443  bposlem1  20523  bposlem2  20524  bposlem9  20531  gx0  20928  gx1  20929  gxm1  20935  gxnn0add  20941  gxnn0mul  20944  ipasslem1  21409  ipasslem2  21410  ipasslem11  21418  minvecolem2  21454  minvecolem3  21455  minvecolem4  21459  shsva  21899  h1datomi  22160  lnfnmuli  22624  leopsq  22709  nmopleid  22719  opsqrlem6  22725  pjnmopi  22728  hstle  22810  csmdsymi  22914  atcvatlem  22965  elsx  23525  cvmliftphtlem  23848  nofulllem4  24359  axlowdimlem6  24575  axlowdimlem14  24583  axcontlem2  24593  fvray  24764  fvline  24767  bpoly2  24792  bpoly3  24793  fsumcube  24795  cbcpcp  25162  mslb1  25607  msra3  25609  cmp2morp  25958  tailfb  26326  heiborlem7  26541  igenidl  26688  eldioph4b  26894  diophren  26896  rmxp1  27017  rmyp1  27018  rmxm1  27019  rmym1  27020  wepwso  27139  frlmlbs  27249  lindfres  27293  lmisfree  27312  onetansqsecsq  28231  cotsqcscsq  28232  dpfrac1  28242  atlatmstc  29509  dihglblem2N  31484
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator