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  3450  frminex  4373  opthreg  7319  unsnen  8175  axcnre  8786  addgt0  9260  addgegt0  9261  addgtge0  9262  addge0  9263  addgt0i  9312  addge0i  9313  addgegt0i  9314  add20i  9316  mulge0i  9320  recextlem1  9398  recne0  9437  recdiv  9466  rec11i  9501  recgt1  9652  prodgt0i  9663  prodge0i  9664  xadddi2  10617  iccshftri  10770  iccshftli  10772  iccdili  10774  icccntri  10776  mulexpz  11142  expaddz  11146  iexpcyc  11207  cnpart  11725  resqrex  11736  sqreulem  11843  amgm2  11853  rlim  11969  ello12  11990  elo12  12001  efcllem  12359  ege2le3  12371  dvdslelem  12573  divalglem1  12593  divalglem6  12597  divalglem9  12600  gcdaddmlem  12707  sqnprm  12777  prmlem1  13109  prmlem2  13121  xpscfn  13461  gzrngunitlem  16436  lmres  17028  zdis  18322  iihalf1  18429  lmclimf  18729  vitali  18968  ismbf  18985  ismbfcn  18986  mbfconst  18990  cncombf  19013  cnmbf  19014  limcfval  19222  dvnfre  19301  quotlem  19680  ulmval  19759  ulmpm  19762  abelthlem2  19808  abelthlem3  19809  abelthlem5  19811  abelthlem7  19814  efcvx  19825  logtayl  20007  logccv  20010  cxpcn3  20088  emcllem2  20290  basellem5  20322  bposlem7  20529  chebbnd1lem3  20620  dchrisumlem3  20640  nv1  21242  blocnilem  21382  ipasslem8  21415  siii  21431  ubthlem1  21449  norm1  21828  hhshsslem2  21845  hoscli  22342  hodcli  22343  cnlnadjlem7  22653  adjbdln  22663  pjnmopi  22728  strlem1  22830  rexdiv  23109  zetacvg  23689  subfacval3  23720  erdszelem4  23725  erdszelem8  23729  rdgprc  24151  tz6.26i  24206  wfii  24208  frindi  24244  axcontlem2  24593  caures  26476  m1expaddsub  27421  psgnuni  27422
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