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

Theorem mpd3an23 1281
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 20 . 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 1184 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  rankcf  8642  bcpasc  11602  swrdid  11762  sqreulem  12153  qnumdencoprm  13127  qeqnumdivden  13128  xpsaddlem  13790  xpsvsca  13794  xpsle  13796  grpinvid  14846  divs0  14988  ghmid  15002  lsm01  15293  frgpadd  15385  abvneg  15912  lsmcv  16203  discmp  17451  kgenhaus  17566  idnghm  18767  xmetdcn2  18858  pi1addval  19063  ipcau2  19181  grpoinvid  21810  ballotlem1ri  24782  pellfundex  26903  stoweidlem21  27701  stoweidlem23  27703  stoweidlem32  27712  stoweidlem36  27716  stoweidlem40  27720  stoweidlem41  27721  opoc1  29901  opoc0  29902  dochsat  32082  lcfrlem9  32249
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  df-3an 938
  Copyright terms: Public domain W3C validator