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

Theorem mp2d 41
Description: A double modus ponens deduction. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
Hypotheses
Ref Expression
mp2d.1  |-  ( ph  ->  ps )
mp2d.2  |-  ( ph  ->  ch )
mp2d.3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
mp2d  |-  ( ph  ->  th )

Proof of Theorem mp2d
StepHypRef Expression
1 mp2d.1 . 2  |-  ( ph  ->  ps )
2 mp2d.2 . . 3  |-  ( ph  ->  ch )
3 mp2d.3 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
42, 3mpid 37 . 2  |-  ( ph  ->  ( ps  ->  th )
)
51, 4mpd 14 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  marypha1lem  7273  wemaplem3  7350  xpwdomg  7386  wrdind  11567  sqr2irr  12618  coprm  12870  efgredlemd  15146  efgredlem  15149  efgred  15150  nmoleub2lem3  18694  iscmet3  18817  derangenlem  24106  symggen  26734  vdfrgragt2  27844  vdgfrgragt2  27845  bnj1145  28768  l1cvpat  29296  llnexchb2  30110  hdmapglem7  32174
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator