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

Theorem mp3an2 1265
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 1151 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 662 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mp3anl2  1272  tz7.7  4455  ordin  4459  onfr  4468  tfrlem11  6446  epfrs  7458  zorng  8176  tsk2  8432  tskcard  8448  gruina  8485  muladd11  9027  00id  9032  negsub  9140  subneg  9141  muleqadd  9457  diveq1  9499  conjmul  9522  recp1lt1  9699  nnsub  9829  addltmul  9994  nnunb  10008  zltp1le  10114  gtndiv  10136  eluzp1m1  10298  zbtwnre  10361  rebtwnz  10362  supxrbnd  10694  flbi2  10994  fldiv  11011  modid  11040  fzen2  11078  nn0ennn  11088  seqshft2  11119  seqf1olem1  11132  ser1const  11149  sq01  11270  expnbnd  11277  faclbnd3  11352  faclbnd5  11358  hashunsng  11414  hashxplem  11432  ccatrid  11482  sqrlem2  11776  sqrlem7  11781  leabs  11831  abs2dif  11863  cvgrat  12386  cos2t  12505  sin01gt0  12517  cos01gt0  12518  demoivre  12527  demoivreALT  12528  znnenlem  12537  rpnnen2lem5  12544  rpnnen2  12551  gcd0id  12749  sqgcd  12784  isprm3  12814  eulerthlem2  12897  omeo  12914  pczpre  12947  pcrec  12958  ressress  13252  mulgm1  14635  gsumsn  15269  unitgrpid  15500  cmpcov2  17173  ufileu  17666  tgpconcompeqg  17846  itg2ge0  19143  abssinper  19939  ppiub  20496  chtub  20504  bposlem2  20577  lgs1  20630  vc0  21180  vcm  21182  vcnegsubdi2  21186  vcsub4  21187  nvmval2  21256  nvzs  21258  nvmf  21259  nvmdi  21263  nvnegneg  21264  nvsubadd  21268  nvpncan2  21269  nvaddsub4  21274  nvnncan  21276  nvm1  21285  nvdif  21286  nvpi  21287  nvz0  21289  nvmtri  21292  nvabs  21294  nvge0  21295  imsmetlem  21314  4ipval2  21336  ipval3  21337  ipidsq  21341  dipcj  21345  sspmval  21364  ipasslem1  21464  ipasslem2  21465  dipsubdir  21481  hvsubdistr1  21683  shsubcl  21855  shsel3  21949  shunssi  22002  hosubdi  22443  lnopmi  22635  nmophmi  22666  nmopcoi  22730  opsqrlem6  22780  hstle  22865  hst0  22868  mdsl2i  22957  superpos  22989  dmdbr5ati  23057  cvmliftphtlem  24132  divelunit  24366  fznatpl1  24379  wfrlem14  24654  colinearalglem4  24923  axsegconlem1  24931  axpaschlem  24954  axcontlem2  24979  axcontlem4  24981  axcontlem7  24984  axcontlem8  24985  elnnrabdioph  26036  rabren3dioph  26046  zindbi  26179  expgrowth  26700  trelpss  26808  2pthon3v  27500  sgnn  27700  atlatle  29328  pmaple  29768  dihglblem2N  31302
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