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  7259  marypha1lem  9192  wemaplem3  9307  xpwdomg  9344  wrdind  14435  wrd2ind  14436  sqrt2irr  15958  coprm  16416  oddprmdvds  16604  cyccom  18822  symggen  19078  efgredlemd  19350  efgredlem  19353  efgred  19354  chcoeffeq  22035  nmoleub2lem3  24278  iscmet3  24457  axtgcgrid  26824  axtg5seg  26826  axtgbtwnid  26827  wlk1walk  28006  umgr2wlk  28314  frgrnbnb  28657  friendshipgt3  28762  ismntd  31262  archiexdiv  31444  fedgmullem2  31711  unelsiga  32102  sibfof  32307  bnj1145  32973  derangenlem  33133  irrdiff  35497  l1cvpat  37068  llnexchb2  37883  hdmapglem7  39943  eel11111  42343  dmrelrnrel  42765  climrec  43144  lptre2pt  43181  0ellimcdiv  43190  iccpartlt  44876