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

Theorem mp2d 43
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 39 . 2  |-  ( ph  ->  ( ps  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  marypha1lem  7396  wemaplem3  7473  xpwdomg  7509  wrdind  11746  sqr2irr  12803  coprm  13055  efgredlemd  15331  efgredlem  15334  efgred  15335  nmoleub2lem3  19076  iscmet3  19199  ofldadd  24191  unelsiga  24470  sibfof  24607  derangenlem  24810  symggen  27279  climrec  27596  frgranbnb  28124  vdgfrgragt2  28132  eel11111  28544  bnj1145  29068  l1cvpat  29537  llnexchb2  30351  hdmapglem7  32415
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator