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

Theorem mpd3an23 1279
Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
Hypotheses
Ref Expression
mpd3an23.1  |-  ( ph  ->  ps )
mpd3an23.2  |-  ( ph  ->  ch )
mpd3an23.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mpd3an23  |-  ( ph  ->  th )

Proof of Theorem mpd3an23
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
2 mpd3an23.1 . 2  |-  ( ph  ->  ps )
3 mpd3an23.2 . 2  |-  ( ph  ->  ch )
4 mpd3an23.3 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  rankcf  8415  bcpasc  11349  swrdid  11474  sqreulem  11859  qnumdencoprm  12832  qeqnumdivden  12833  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  grpinvid  14549  divs0  14691  ghmid  14705  lsm01  14996  frgpadd  15088  abvneg  15615  lsmcv  15910  discmp  17141  kgenhaus  17255  idnghm  18268  xmetdcn2  18358  pi1addval  18562  ipcau2  18680  grpoinvid  20915  ballotlem1ri  23109  pellfundex  27074  opoc1  30014  opoc0  30015  dochsat  32195  lcfrlem9  32362
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  df-3an 936
  Copyright terms: Public domain W3C validator