MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpd3an23 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  8578  bcpasc  11532  swrdid  11692  sqreulem  12083  qnumdencoprm  13057  qeqnumdivden  13058  xpsaddlem  13720  xpsvsca  13724  xpsle  13726  grpinvid  14776  divs0  14918  ghmid  14932  lsm01  15223  frgpadd  15315  abvneg  15842  lsmcv  16133  discmp  17376  kgenhaus  17490  idnghm  18641  xmetdcn2  18732  pi1addval  18937  ipcau2  19055  grpoinvid  21661  ballotlem1ri  24564  pellfundex  26633  stoweidlem21  27431  stoweidlem23  27433  stoweidlem32  27442  stoweidlem36  27446  stoweidlem40  27450  stoweidlem41  27451  opoc1  29368  opoc0  29369  dochsat  31549  lcfrlem9  31716
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