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  7891  wemaplem3  7971  xpwdomg  8009  wrdind  12676  wrd2ind  12677  sqrt2irr  13854  coprm  14113  symggen  16364  efgredlemd  16631  efgredlem  16634  efgred  16635  chcoeffeq  19254  nmoleub2lem3  21464  iscmet3  21598  axtgcgrid  23725  axtg5seg  23727  axtgbtwnid  23728  frgranbnb  24885  vdgfrgragt2  24892  friendshipgt3  24986  archiexdiv  27600  unelsiga  28000  sibfof  28148  derangenlem  28481  climrec  31513  lptre2pt  31550  0ellimcdiv  31559  eel11111  33228  bnj1145  33756  l1cvpat  34481  llnexchb2  35295  hdmapglem7  37361
  Copyright terms: Public domain W3C validator