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  7675  wemaplem3  7754  xpwdomg  7792  wrdind  12363  wrd2ind  12364  sqr2irr  13523  coprm  13778  symggen  15967  efgredlemd  16232  efgredlem  16235  efgred  16236  nmoleub2lem3  20650  iscmet3  20784  axtgcgrid  22904  axtgbtwnid  22907  unelsiga  26546  sibfof  26695  derangenlem  27028  climrec  29747  frgranbnb  30583  vdgfrgragt2  30591  friendshipgt3  30685  eel11111  31385  bnj1145  31913  l1cvpat  32592  llnexchb2  33406  hdmapglem7  35470
  Copyright terms: Public domain W3C validator