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

Theorem mpanl12 664
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mpanl12.1  |-  ph
mpanl12.2  |-  ps
mpanl12.3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
mpanl12  |-  ( ch 
->  th )

Proof of Theorem mpanl12
StepHypRef Expression
1 mpanl12.2 . 2  |-  ps
2 mpanl12.1 . . 3  |-  ph
3 mpanl12.3 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3mpanl1 662 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 652 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  reuun1  3559  frminex  4496  opthreg  7499  unsnen  8354  axcnre  8965  addgt0  9439  addgegt0  9440  addgtge0  9441  addge0  9442  addgt0i  9491  addge0i  9492  addgegt0i  9493  add20i  9495  mulge0i  9499  recextlem1  9577  recne0  9616  recdiv  9645  rec11i  9680  recgt1  9831  prodgt0i  9842  prodge0i  9843  xadddi2  10801  iccshftri  10956  iccshftli  10958  iccdili  10960  icccntri  10962  mulexpz  11340  expaddz  11344  iexpcyc  11405  cnpart  11965  resqrex  11976  sqreulem  12083  amgm2  12093  rlim  12209  ello12  12230  elo12  12241  efcllem  12600  ege2le3  12612  dvdslelem  12814  divalglem1  12834  divalglem6  12838  divalglem9  12841  gcdaddmlem  12948  sqnprm  13018  prmlem1  13350  prmlem2  13362  xpscfn  13704  gzrngunitlem  16679  lmres  17279  zdis  18711  iihalf1  18820  lmclimf  19120  vitali  19365  ismbf  19382  ismbfcn  19383  mbfconst  19387  cncombf  19410  cnmbf  19411  limcfval  19619  dvnfre  19698  quotlem  20077  ulmval  20156  ulmpm  20159  abelthlem2  20208  abelthlem3  20209  abelthlem5  20211  abelthlem7  20214  efcvx  20225  logtayl  20411  logccv  20414  cxpcn3  20492  emcllem2  20695  basellem5  20727  bposlem7  20934  chebbnd1lem3  21025  dchrisumlem3  21045  nv1  22006  blocnilem  22146  ipasslem8  22179  siii  22195  ubthlem1  22213  norm1  22592  hhshsslem2  22609  hoscli  23106  hodcli  23107  cnlnadjlem7  23417  adjbdln  23427  pjnmopi  23492  strlem1  23594  rexdiv  24003  tpr2rico  24107  qqhre  24175  zetacvg  24571  subfacval3  24647  erdszelem4  24652  erdszelem8  24656  m1expevenALT  24677  rdgprc  25168  tz6.26i  25223  wfii  25225  frindi  25261  axcontlem2  25611  caures  26150  m1expaddsub  27083  psgnuni  27084
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
  Copyright terms: Public domain W3C validator