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

Theorem mp3an2 1267
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
Hypotheses
Ref Expression
mp3an2.1  |-  ps
mp3an2.2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an2  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mp3an2
StepHypRef Expression
1 mp3an2.1 . 2  |-  ps
2 mp3an2.2 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
323expa 1153 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 663 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mp3anl2  1274  tz7.7  4599  ordin  4603  onfr  4612  tfrlem11  6641  epfrs  7659  zorng  8376  tsk2  8632  tskcard  8648  gruina  8685  muladd11  9228  00id  9233  negsub  9341  subneg  9342  muleqadd  9658  diveq1  9700  conjmul  9723  recp1lt1  9900  nnsub  10030  addltmul  10195  nnunb  10209  zltp1le  10317  gtndiv  10339  eluzp1m1  10501  zbtwnre  10564  rebtwnz  10565  supxrbnd  10899  flbi2  11216  fldiv  11233  modid  11262  fzen2  11300  nn0ennn  11310  seqshft2  11341  seqf1olem1  11354  ser1const  11371  sq01  11493  expnbnd  11500  faclbnd3  11575  faclbnd5  11581  hashunsng  11657  hashxplem  11688  ccatrid  11741  sqrlem2  12041  sqrlem7  12046  leabs  12096  abs2dif  12128  cvgrat  12652  cos2t  12771  sin01gt0  12783  cos01gt0  12784  demoivre  12793  demoivreALT  12794  znnenlem  12803  rpnnen2lem5  12810  rpnnen2  12817  gcd0id  13015  sqgcd  13050  isprm3  13080  eulerthlem2  13163  omeo  13180  pczpre  13213  pcrec  13224  ressress  13518  mulgm1  14901  gsumsn  15535  unitgrpid  15766  cmpcov2  17445  ufileu  17943  tgpconcompeqg  18133  itg2ge0  19619  abssinper  20418  ppiub  20980  chtub  20988  bposlem2  21061  lgs1  21114  constr2spthlem1  21586  2pthon3v  21596  vc0  22040  vcm  22042  vcnegsubdi2  22046  vcsub4  22047  nvmval2  22116  nvzs  22118  nvmf  22119  nvmdi  22123  nvnegneg  22124  nvsubadd  22128  nvpncan2  22129  nvaddsub4  22134  nvnncan  22136  nvm1  22145  nvdif  22146  nvpi  22147  nvz0  22149  nvmtri  22152  nvabs  22154  nvge0  22155  imsmetlem  22174  4ipval2  22196  ipval3  22197  ipidsq  22201  dipcj  22205  sspmval  22224  ipasslem1  22324  ipasslem2  22325  dipsubdir  22341  hvsubdistr1  22543  shsubcl  22715  shsel3  22809  shunssi  22862  hosubdi  23303  lnopmi  23495  nmophmi  23526  nmopcoi  23590  opsqrlem6  23640  hstle  23725  hst0  23728  mdsl2i  23817  superpos  23849  dmdbr5ati  23917  cvmliftphtlem  24996  divelunit  25177  fznatpl1  25190  wfrlem14  25543  colinearalglem4  25840  axsegconlem1  25848  axpaschlem  25871  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem8  25902  mblfinlem  26234  mblfinlem3  26236  ismblfin  26237  elnnrabdioph  26858  rabren3dioph  26867  zindbi  27000  expgrowth  27520  trelpss  27627  el2spthonot  28290  el2spthonot0  28291  frg2woteq  28386  sgnn  28461  atlatle  30055  pmaple  30495  dihglblem2N  32029
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