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  4418  ordin  4422  onfr  4431  tfrlem11  6404  epfrs  7413  zorng  8131  tsk2  8387  tskcard  8403  gruina  8440  muladd11  8982  00id  8987  negsub  9095  subneg  9096  muleqadd  9412  diveq1  9454  conjmul  9477  recp1lt1  9654  nnsub  9784  addltmul  9947  nnunb  9961  zltp1le  10067  gtndiv  10089  eluzp1m1  10251  zbtwnre  10314  rebtwnz  10315  supxrbnd  10647  flbi2  10947  fldiv  10964  modid  10993  fzen2  11031  nn0ennn  11041  seqshft2  11072  seqf1olem1  11085  ser1const  11102  sq01  11223  expnbnd  11230  faclbnd3  11305  faclbnd5  11311  hashunsng  11367  hashxplem  11385  ccatrid  11435  sqrlem2  11729  sqrlem7  11734  leabs  11784  abs2dif  11816  cvgrat  12339  cos2t  12458  sin01gt0  12470  cos01gt0  12471  demoivre  12480  demoivreALT  12481  znnenlem  12490  rpnnen2lem5  12497  rpnnen2  12504  gcd0id  12702  sqgcd  12737  isprm3  12767  eulerthlem2  12850  omeo  12867  pczpre  12900  pcrec  12911  ressress  13205  mulgm1  14586  gsumsn  15220  unitgrpid  15451  cmpcov2  17117  ufileu  17614  tgpconcompeqg  17794  itg2ge0  19090  abssinper  19886  ppiub  20443  chtub  20451  bposlem2  20524  lgs1  20577  vc0  21125  vcm  21127  vcnegsubdi2  21131  vcsub4  21132  nvmval2  21201  nvzs  21203  nvmf  21204  nvmdi  21208  nvnegneg  21209  nvsubadd  21213  nvpncan2  21214  nvaddsub4  21219  nvnncan  21221  nvm1  21230  nvdif  21231  nvpi  21232  nvz0  21234  nvmtri  21237  nvabs  21239  nvge0  21240  imsmetlem  21259  4ipval2  21281  ipval3  21282  ipidsq  21286  dipcj  21290  sspmval  21309  ipasslem1  21409  ipasslem2  21410  dipsubdir  21426  hvsubdistr1  21628  shsubcl  21800  shsel3  21894  shunssi  21947  hosubdi  22388  lnopmi  22580  nmophmi  22611  nmopcoi  22675  opsqrlem6  22725  hstle  22810  hst0  22813  mdsl2i  22902  superpos  22934  dmdbr5ati  23002  cvmliftphtlem  23848  divelunit  24080  fznatpl1  24093  wfrlem14  24269  colinearalglem4  24537  axsegconlem1  24545  axpaschlem  24568  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  mulone  25685  elnnrabdioph  26888  rabren3dioph  26898  zindbi  27031  expgrowth  27552  trelpss  27660  tz6.12-afv  28035  sgnn  28251  atlatle  29510  pmaple  29950  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