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

Theorem mp2d 45
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 41 . 2  |-  ( ph  ->  ( ps  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  marypha1lem  7784  wemaplem3  7863  xpwdomg  7901  wrdind  12473  wrd2ind  12474  sqr2irr  13633  coprm  13888  symggen  16078  efgredlemd  16345  efgredlem  16348  efgred  16349  nmoleub2lem3  20786  iscmet3  20920  axtgcgrid  23040  axtgbtwnid  23043  unelsiga  26711  sibfof  26860  derangenlem  27193  climrec  29914  frgranbnb  30750  vdgfrgragt2  30758  friendshipgt3  30852  eel11111  31756  bnj1145  32284  l1cvpat  33005  llnexchb2  33819  hdmapglem7  35883
  Copyright terms: Public domain W3C validator