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  7325  marypha1lem  9295  wemaplem3  9410  xpwdomg  9447  wrdind  14534  wrd2ind  14535  sqrt2irr  16058  coprm  16514  oddprmdvds  16702  cyccom  18919  symggen  19175  efgredlemd  19446  efgredlem  19449  efgred  19450  chcoeffeq  22141  nmoleub2lem3  24384  iscmet3  24563  axtgcgrid  27113  axtg5seg  27115  axtgbtwnid  27116  wlk1walk  28295  umgr2wlk  28602  frgrnbnb  28945  friendshipgt3  29050  ismntd  31547  archiexdiv  31729  fedgmullem2  32007  unelsiga  32398  sibfof  32605  bnj1145  33270  derangenlem  33430  irrdiff  35651  l1cvpat  37370  llnexchb2  38186  hdmapglem7  40246  eel11111  42714  dmrelrnrel  43143  climrec  43530  lptre2pt  43567  0ellimcdiv  43576  iccpartlt  45292