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  7671  wemaplem3  7750  xpwdomg  7788  wrdind  12355  wrd2ind  12356  sqr2irr  13514  coprm  13769  symggen  15956  efgredlemd  16221  efgredlem  16224  efgred  16225  nmoleub2lem3  20512  iscmet3  20646  axtgcgrid  22809  axtgbtwnid  22812  unelsiga  26431  sibfof  26574  derangenlem  26907  climrec  29622  frgranbnb  30458  vdgfrgragt2  30466  friendshipgt3  30560  eel11111  31158  bnj1145  31686  l1cvpat  32272  llnexchb2  33086  hdmapglem7  35150
  Copyright terms: Public domain W3C validator