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

Theorem mpanl12 663
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 661 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 651 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  reuun1  3463  frminex  4389  opthreg  7335  unsnen  8191  axcnre  8802  addgt0  9276  addgegt0  9277  addgtge0  9278  addge0  9279  addgt0i  9328  addge0i  9329  addgegt0i  9330  add20i  9332  mulge0i  9336  recextlem1  9414  recne0  9453  recdiv  9482  rec11i  9517  recgt1  9668  prodgt0i  9679  prodge0i  9680  xadddi2  10633  iccshftri  10786  iccshftli  10788  iccdili  10790  icccntri  10792  mulexpz  11158  expaddz  11162  iexpcyc  11223  cnpart  11741  resqrex  11752  sqreulem  11859  amgm2  11869  rlim  11985  ello12  12006  elo12  12017  efcllem  12375  ege2le3  12387  dvdslelem  12589  divalglem1  12609  divalglem6  12613  divalglem9  12616  gcdaddmlem  12723  sqnprm  12793  prmlem1  13125  prmlem2  13137  xpscfn  13477  gzrngunitlem  16452  lmres  17044  zdis  18338  iihalf1  18445  lmclimf  18745  vitali  18984  ismbf  19001  ismbfcn  19002  mbfconst  19006  cncombf  19029  cnmbf  19030  limcfval  19238  dvnfre  19317  quotlem  19696  ulmval  19775  ulmpm  19778  abelthlem2  19824  abelthlem3  19825  abelthlem5  19827  abelthlem7  19830  efcvx  19841  logtayl  20023  logccv  20026  cxpcn3  20104  emcllem2  20306  basellem5  20338  bposlem7  20545  chebbnd1lem3  20636  dchrisumlem3  20656  nv1  21258  blocnilem  21398  ipasslem8  21431  siii  21447  ubthlem1  21465  norm1  21844  hhshsslem2  21861  hoscli  22358  hodcli  22359  cnlnadjlem7  22669  adjbdln  22679  pjnmopi  22744  strlem1  22846  rexdiv  23125  zetacvg  23704  subfacval3  23735  erdszelem4  23740  erdszelem8  23744  rdgprc  24222  tz6.26i  24277  wfii  24279  frindi  24315  axcontlem2  24665  caures  26579  m1expaddsub  27524  psgnuni  27525
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
  Copyright terms: Public domain W3C validator