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

Theorem mpd3an23 1279
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 19 . 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 1182 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  rankcf  8399  bcpasc  11333  swrdid  11458  sqreulem  11843  qnumdencoprm  12816  qeqnumdivden  12817  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  grpinvid  14533  divs0  14675  ghmid  14689  lsm01  14980  frgpadd  15072  abvneg  15599  lsmcv  15894  discmp  17125  kgenhaus  17239  idnghm  18252  xmetdcn2  18342  pi1addval  18546  ipcau2  18664  grpoinvid  20899  ballotlem1ri  23093  pellfundex  26971  opoc1  29392  opoc0  29393  dochsat  31573  lcfrlem9  31740
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator