Theorem mp2d 49

Description: A double modus ponens deduction. Deduction associated with mp2 9. (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

Step	Hyp	Ref	Expression
1		mp2d.1	. 2 |- ( ph -> ps )
2		mp2d.2	. . 3 |- ( ph -> ch )
3		mp2d.3	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	2, 3	mpid 44	. 2 |- ( ph -> ( ps -> th ) )
5	1, 4	mpd 15	1 |- ( ph -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  riotaeqimp  6634  marypha1lem  8339  wemaplem3  8453  xpwdomg  8490  wrdind  13476  wrd2ind  13477  sqrt2irr  14979  coprm  15423  oddprmdvds  15607  symggen  17890  efgredlemd  18157  efgredlem  18160  efgred  18161  chcoeffeq  20691  nmoleub2lem3  22915  iscmet3  23091  axtgcgrid  25362  axtg5seg  25364  axtgbtwnid  25365  wlk1walk  26535  umgr2wlk  26845  frgrnbnb  27157  friendshipgt3  27256  archiexdiv  29744  unelsiga  30197  sibfof  30402  bnj1145  31061  derangenlem  31153  l1cvpat  34341  llnexchb2  35155  hdmapglem7  37221  eel11111  38950  dmrelrnrel  39419  climrec  39835  lptre2pt  39872  0ellimcdiv  39881  iccpartlt  41360