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  7882  wemaplem3  7962  xpwdomg  8000  wrdind  12652  wrd2ind  12653  sqr2irr  13832  coprm  14089  symggen  16284  efgredlemd  16551  efgredlem  16554  efgred  16555  chcoeffeq  19147  nmoleub2lem3  21326  iscmet3  21460  axtgcgrid  23581  axtgbtwnid  23584  unelsiga  27624  sibfof  27772  derangenlem  28105  climrec  30964  frgranbnb  31738  vdgfrgragt2  31746  friendshipgt3  31840  eel11111  32475  bnj1145  33003  l1cvpat  33726  llnexchb2  34540  hdmapglem7  36604
  Copyright terms: Public domain W3C validator