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	⊢ (𝜑 → 𝜓)
mp2d.2	⊢ (𝜑 → 𝜒)
mp2d.3	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
mp2d	⊢ (𝜑 → 𝜃)

Proof of Theorem mp2d

Step	Hyp	Ref	Expression
1		mp2d.1	. 2 ⊢ (𝜑 → 𝜓)
2		mp2d.2	. . 3 ⊢ (𝜑 → 𝜒)
3		mp2d.3	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpid 44	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜃)

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  7396  marypha1lem  9432  wemaplem3  9547  xpwdomg  9584  wrdind  14678  wrd2ind  14679  sqrt2irr  16198  coprm  16654  oddprmdvds  16842  cyccom  19120  symggen  19381  efgredlemd  19655  efgredlem  19658  efgred  19659  chcoeffeq  22610  nmoleub2lem3  24864  iscmet3  25043  mulsproplem1  27809  axtgcgrid  27979  axtg5seg  27981  axtgbtwnid  27982  wlk1walk  29161  umgr2wlk  29468  frgrnbnb  29811  friendshipgt3  29916  ismntd  32419  archiexdiv  32604  fedgmullem2  33001  unelsiga  33428  sibfof  33635  bnj1145  34300  derangenlem  34458  irrdiff  36512  l1cvpat  38229  llnexchb2  39045  hdmapglem7  41105  eel11111  43788  dmrelrnrel  44225  climrec  44619  lptre2pt  44656  0ellimcdiv  44665  iccpartlt  46392