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  4798  ov  6051  ovmpt2a  6062  ovmpt2  6067  oaword1  6634  oneo  6663  oeoalem  6678  oeoelem  6680  nnaword1  6711  nnneo  6733  erov  6840  th3q  6852  enrefg  6978  f1imaen  7008  mapxpen  7112  acnlem  7762  cdacomen  7894  infmap  8285  canthnumlem  8357  tskin  8468  tsksn  8469  tsk0  8472  gruxp  8516  gruina  8527  genpprecl  8712  supsrlem  8820  mulid1  8922  00id  9074  mul02lem1  9075  ltneg  9361  leneg  9364  suble0  9375  div1  9540  nnaddcl  9855  nnmulcl  9856  nnge1  9859  nnsub  9871  2halves  10029  halfaddsub  10034  addltmul  10036  zleltp1  10157  nnaddm1cl  10162  zextlt  10175  uzindOLD  10195  eluzp1p1  10342  uzaddcl  10364  znq  10409  xrre  10587  xrre2  10588  fzshftral  10958  fraclt1  11023  expadd  11234  expmul  11237  expubnd  11252  sqmul  11257  bernneq  11317  faclbnd2  11394  faclbnd6  11402  hashgadd  11449  hashun2  11455  hashssdif  11464  hashfun  11479  ccatlcan  11554  ccatrcan  11555  shftval3  11661  sqrlem1  11818  caubnd2  11931  efexp  12472  efival  12523  cos01gt0  12562  odd2np1  12678  divalglem5  12687  gcdmultiple  12820  sqgcd  12828  nn0seqcvgd  12831  phiprmpw  12935  eulerthlem2  12941  odzcllem  12948  omoe  12956  opeo  12957  pythagtriplem15  12973  pythagtriplem17  12975  pcelnn  13013  4sqlem3  13088  xpscfn  13554  fullfunc  13873  fthfunc  13874  prfcl  14070  curf1cl  14095  curfcl  14099  hofcl  14126  odinv  14967  lsmelvalix  15045  dprdval  15331  lsp0  15859  lss0v  15866  coe1scl  16455  zndvds0  16604  ntrin  16898  lpsscls  16973  restperf  17014  txuni2  17360  txopn  17397  elqtop2  17492  xkocnv  17605  ptcmp  17848  xblpnf  18049  bl2in  18053  unirnbl  18065  blpnfctr  18078  dscopn  18192  bcthlem4  18847  minveclem2  18888  minveclem4  18894  icombl  19019  i1fadd  19148  i1fmul  19149  dvn1  19373  dvexp3  19423  plyconst  19686  plyid  19689  sincosq1eq  19981  sinord  19997  cxpp1  20132  cxpsqrlem  20154  cxpsqr  20155  angneg  20206  dcubic  20247  issqf  20480  ppiub  20549  bposlem1  20629  bposlem2  20630  bposlem9  20637  gx0  21034  gx1  21035  gxm1  21041  gxnn0add  21047  gxnn0mul  21050  ipasslem1  21517  ipasslem2  21518  ipasslem11  21526  minvecolem2  21562  minvecolem3  21563  minvecolem4  21567  shsva  22007  h1datomi  22268  lnfnmuli  22732  leopsq  22817  nmopleid  22827  opsqrlem6  22833  pjnmopi  22836  hstle  22918  csmdsymi  23022  atcvatlem  23073  elsx  23814  dya2iocnrect  23895  cvmliftphtlem  24252  nofulllem4  24917  axlowdimlem6  25134  axlowdimlem14  25142  axcontlem2  25152  fvray  25323  fvline  25326  bpoly2  25351  bpoly3  25352  fsumcube  25354  itgaddnclem2  25499  tailfb  25650  heiborlem7  25864  igenidl  26011  eldioph4b  26217  diophren  26219  rmxp1  26340  rmyp1  26341  rmxm1  26342  rmym1  26343  wepwso  26462  frlmlbs  26572  lindfres  26616  lmisfree  26635  onetansqsecsq  27914  cotsqcscsq  27915  dpfrac1  27925  atlatmstc  29561  dihglblem2N  31536
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