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

Theorem mp2d 44
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 40 . 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  7441  wemaplem3  7520  xpwdomg  7556  wrdind  11796  sqr2irr  12853  coprm  13105  efgredlemd  15381  efgredlem  15384  efgred  15385  nmoleub2lem3  19128  iscmet3  19251  ofldadd  24243  unelsiga  24522  sibfof  24659  derangenlem  24862  symggen  27402  climrec  27719  frgranbnb  28484  vdgfrgragt2  28492  eel11111  28909  bnj1145  29436  l1cvpat  29926  llnexchb2  30740  hdmapglem7  32804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator