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

Theorem mpd3an23 1362
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 23 . 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 1264 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  rankcf  9191  bcpasc  12492  sqreulem  13390  qnumdencoprm  14654  qeqnumdivden  14655  xpsaddlem  15433  xpsvsca  15437  xpsle  15439  grpinvid  16669  qus0  16827  ghmid  16841  lsm01  17262  frgpadd  17354  abvneg  18003  lsmcv  18305  discmp  20350  kgenhaus  20496  idnghm  21701  xmetdcn2  21792  pi1addval  21998  ipcau2  22127  grpoinvid  25846  carsgclctunlem2  29021  carsgclctun  29023  ballotlem1ri  29234  ftc1anclem5  31769  opoc1  32521  opoc0  32522  dochsat  34704  lcfrlem9  34871  pellfundex  35488  0ellimcdiv  37350  stoweidlem21  37498  stoweidlem23  37500  stoweidlem32  37510  stoweidlem36  37514  stoweidlem40  37518  stoweidlem41  37519  lincval0  39025
  Copyright terms: Public domain W3C validator