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

Theorem mpd3an23 1326
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 22 . 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 1228 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  rankcf  9156  bcpasc  12368  lswccat0lsw  12574  swrdid  12618  sqreulem  13158  qnumdencoprm  14140  qeqnumdivden  14141  xpsaddlem  14833  xpsvsca  14837  xpsle  14839  grpinvid  15915  qus0  16073  ghmid  16087  lsm01  16504  frgpadd  16596  abvneg  17295  lsmcv  17599  discmp  19704  kgenhaus  19872  idnghm  21077  xmetdcn2  21169  pi1addval  21375  ipcau2  21504  grpoinvid  25007  ballotlem1ri  28224  ftc1anclem5  29947  pellfundex  30653  stoweidlem21  31548  stoweidlem23  31550  stoweidlem32  31559  stoweidlem36  31563  stoweidlem40  31567  stoweidlem41  31568  lincval0  32314  opoc1  34216  opoc0  34217  dochsat  36397  lcfrlem9  36564
  Copyright terms: Public domain W3C validator