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

Theorem mp3an2 1268
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 1154 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
41, 3mpanl2 664 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  mp3anl2  1275  tz7.7  4610  ordin  4614  onfr  4623  tfrlem11  6652  epfrs  7670  zorng  8389  tsk2  8645  tskcard  8661  gruina  8698  muladd11  9241  00id  9246  negsub  9354  subneg  9355  muleqadd  9671  diveq1  9713  conjmul  9736  recp1lt1  9913  nnsub  10043  addltmul  10208  nnunb  10222  zltp1le  10330  gtndiv  10352  eluzp1m1  10514  zbtwnre  10577  rebtwnz  10578  supxrbnd  10912  flbi2  11229  fldiv  11246  modid  11275  fzen2  11313  nn0ennn  11323  seqshft2  11354  seqf1olem1  11367  ser1const  11384  sq01  11506  expnbnd  11513  faclbnd3  11588  faclbnd5  11594  hashunsng  11670  hashxplem  11701  ccatrid  11754  sqrlem2  12054  sqrlem7  12059  leabs  12109  abs2dif  12141  cvgrat  12665  cos2t  12784  sin01gt0  12796  cos01gt0  12797  demoivre  12806  demoivreALT  12807  znnenlem  12816  rpnnen2lem5  12823  rpnnen2  12830  gcd0id  13028  sqgcd  13063  isprm3  13093  eulerthlem2  13176  omeo  13193  pczpre  13226  pcrec  13237  ressress  13531  mulgm1  14914  gsumsn  15548  unitgrpid  15779  cmpcov2  17458  ufileu  17956  tgpconcompeqg  18146  itg2ge0  19630  abssinper  20431  ppiub  20993  chtub  21001  bposlem2  21074  lgs1  21127  constr2spthlem1  21599  2pthon3v  21609  vc0  22053  vcm  22055  vcnegsubdi2  22059  vcsub4  22060  nvmval2  22129  nvzs  22131  nvmf  22132  nvmdi  22136  nvnegneg  22137  nvsubadd  22141  nvpncan2  22142  nvaddsub4  22147  nvnncan  22149  nvm1  22158  nvdif  22159  nvpi  22160  nvz0  22162  nvmtri  22165  nvabs  22167  nvge0  22168  imsmetlem  22187  4ipval2  22209  ipval3  22210  ipidsq  22214  dipcj  22218  sspmval  22237  ipasslem1  22337  ipasslem2  22338  dipsubdir  22354  hvsubdistr1  22556  shsubcl  22728  shsel3  22822  shunssi  22875  hosubdi  23316  lnopmi  23508  nmophmi  23539  nmopcoi  23603  opsqrlem6  23653  hstle  23738  hst0  23741  mdsl2i  23830  superpos  23862  dmdbr5ati  23930  cvmliftphtlem  25009  divelunit  25190  fznatpl1  25203  wfrlem14  25556  colinearalglem4  25853  axsegconlem1  25861  axpaschlem  25884  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  tan2h  26252  mblfinlem2  26256  mblfinlem4  26258  ismblfin  26259  elnnrabdioph  26881  rabren3dioph  26890  zindbi  27023  expgrowth  27543  trelpss  27650  el2spthonot  28402  el2spthonot0  28403  frg2woteq  28523  sgnn  28598  atlatle  30192  pmaple  30632  dihglblem2N  32166
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator