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  7239  marypha1lem  9122  wemaplem3  9237  xpwdomg  9274  wrdind  14363  wrd2ind  14364  sqrt2irr  15886  coprm  16344  oddprmdvds  16532  cyccom  18737  symggen  18993  efgredlemd  19265  efgredlem  19268  efgred  19269  chcoeffeq  21943  nmoleub2lem3  24184  iscmet3  24362  axtgcgrid  26728  axtg5seg  26730  axtgbtwnid  26731  wlk1walk  27908  umgr2wlk  28215  frgrnbnb  28558  friendshipgt3  28663  ismntd  31164  archiexdiv  31346  fedgmullem2  31613  unelsiga  32002  sibfof  32207  bnj1145  32873  derangenlem  33033  irrdiff  35424  l1cvpat  36995  llnexchb2  37810  hdmapglem7  39870  eel11111  42232  dmrelrnrel  42654  climrec  43034  lptre2pt  43071  0ellimcdiv  43080  iccpartlt  44764