MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanl12 Structured version   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  3615  frminex  4554  opthreg  7565  unsnen  8420  axcnre  9031  addgt0  9506  addgegt0  9507  addgtge0  9508  addge0  9509  addgt0i  9558  addge0i  9559  addgegt0i  9560  add20i  9562  mulge0i  9566  recextlem1  9644  recne0  9683  recdiv  9712  rec11i  9747  recgt1  9898  prodgt0i  9909  prodge0i  9910  xadddi2  10868  iccshftri  11023  iccshftli  11025  iccdili  11027  icccntri  11029  mulexpz  11412  expaddz  11416  iexpcyc  11477  cnpart  12037  resqrex  12048  sqreulem  12155  amgm2  12165  rlim  12281  ello12  12302  elo12  12313  efcllem  12672  ege2le3  12684  dvdslelem  12886  divalglem1  12906  divalglem6  12910  divalglem9  12913  gcdaddmlem  13020  sqnprm  13090  prmlem1  13422  prmlem2  13434  xpscfn  13776  gzrngunitlem  16755  lmres  17356  zdis  18839  iihalf1  18948  lmclimf  19248  vitali  19497  ismbf  19514  ismbfcn  19515  mbfconst  19519  cncombf  19542  cnmbf  19543  limcfval  19751  dvnfre  19830  quotlem  20209  ulmval  20288  ulmpm  20291  abelthlem2  20340  abelthlem3  20341  abelthlem5  20343  abelthlem7  20346  efcvx  20357  logtayl  20543  logccv  20546  cxpcn3  20624  emcllem2  20827  basellem5  20859  bposlem7  21066  chebbnd1lem3  21157  dchrisumlem3  21177  nv1  22157  blocnilem  22297  ipasslem8  22330  siii  22346  ubthlem1  22364  norm1  22743  hhshsslem2  22760  hoscli  23257  hodcli  23258  cnlnadjlem7  23568  adjbdln  23578  pjnmopi  23643  strlem1  23745  rexdiv  24164  tpr2rico  24302  qqhre  24378  zetacvg  24791  subfacval3  24867  erdszelem4  24872  erdszelem8  24876  m1expevenALT  24897  rdgprc  25414  tz6.26i  25473  wfii  25475  frindi  25511  axcontlem2  25896  ismblfin  26237  itg2addnclem  26246  caures  26457  m1expaddsub  27389  psgnuni  27390
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