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

Theorem mpd3an23 1317
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 1219 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  rankcf  9058  bcpasc  12217  lswccat0lsw  12409  swrdid  12442  sqreulem  12968  qnumdencoprm  13944  qeqnumdivden  13945  xpsaddlem  14635  xpsvsca  14639  xpsle  14641  grpinvid  15711  divs0  15861  ghmid  15875  lsm01  16292  frgpadd  16384  abvneg  17045  lsmcv  17348  discmp  19136  kgenhaus  19252  idnghm  20457  xmetdcn2  20549  pi1addval  20755  ipcau2  20884  grpoinvid  23891  ballotlem1ri  27081  ftc1anclem5  28639  pellfundex  29395  stoweidlem21  29984  stoweidlem23  29986  stoweidlem32  29995  stoweidlem36  29999  stoweidlem40  30003  stoweidlem41  30004  lincval0  31101  opoc1  33205  opoc0  33206  dochsat  35386  lcfrlem9  35553
  Copyright terms: Public domain W3C validator