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  3583  frminex  4522  opthreg  7529  unsnen  8384  axcnre  8995  addgt0  9470  addgegt0  9471  addgtge0  9472  addge0  9473  addgt0i  9522  addge0i  9523  addgegt0i  9524  add20i  9526  mulge0i  9530  recextlem1  9608  recne0  9647  recdiv  9676  rec11i  9711  recgt1  9862  prodgt0i  9873  prodge0i  9874  xadddi2  10832  iccshftri  10987  iccshftli  10989  iccdili  10991  icccntri  10993  mulexpz  11375  expaddz  11379  iexpcyc  11440  cnpart  12000  resqrex  12011  sqreulem  12118  amgm2  12128  rlim  12244  ello12  12265  elo12  12276  efcllem  12635  ege2le3  12647  dvdslelem  12849  divalglem1  12869  divalglem6  12873  divalglem9  12876  gcdaddmlem  12983  sqnprm  13053  prmlem1  13385  prmlem2  13397  xpscfn  13739  gzrngunitlem  16718  lmres  17318  zdis  18800  iihalf1  18909  lmclimf  19209  vitali  19458  ismbf  19475  ismbfcn  19476  mbfconst  19480  cncombf  19503  cnmbf  19504  limcfval  19712  dvnfre  19791  quotlem  20170  ulmval  20249  ulmpm  20252  abelthlem2  20301  abelthlem3  20302  abelthlem5  20304  abelthlem7  20307  efcvx  20318  logtayl  20504  logccv  20507  cxpcn3  20585  emcllem2  20788  basellem5  20820  bposlem7  21027  chebbnd1lem3  21118  dchrisumlem3  21138  nv1  22118  blocnilem  22258  ipasslem8  22291  siii  22307  ubthlem1  22325  norm1  22704  hhshsslem2  22721  hoscli  23218  hodcli  23219  cnlnadjlem7  23529  adjbdln  23539  pjnmopi  23604  strlem1  23706  rexdiv  24125  tpr2rico  24263  qqhre  24339  zetacvg  24752  subfacval3  24828  erdszelem4  24833  erdszelem8  24837  m1expevenALT  24858  rdgprc  25365  tz6.26i  25420  wfii  25422  frindi  25458  axcontlem2  25808  ismblfin  26146  itg2addnclem  26155  caures  26356  m1expaddsub  27289  psgnuni  27290
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