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  7186  wemaplem3  7263  xpwdomg  7299  wrdind  11477  sqr2irr  12527  coprm  12779  efgredlemd  15053  efgredlem  15056  efgred  15057  nmoleub2lem3  18596  iscmet3  18719  derangenlem  23702  preotr2  25235  negveud  25668  negveudr  25669  symggen  27411  bnj1145  29023  l1cvpat  29244  llnexchb2  30058  hdmapglem7  32122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator