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  6894  marypha1lem  8614  wemaplem3  8729  xpwdomg  8766  wrdind  13819  wrdindOLD  13820  wrd2ind  13821  wrd2indOLD  13822  sqrt2irr  15359  coprm  15801  oddprmdvds  15985  symggen  18247  efgredlemd  18516  efgredlem  18519  efgredlemOLD  18520  efgred  18521  chcoeffeq  21068  nmoleub2lem3  23291  iscmet3  23468  axtgcgrid  25782  axtg5seg  25784  axtgbtwnid  25785  wlk1walk  26943  umgr2wlk  27285  frgrnbnb  27670  friendshipgt3  27809  archiexdiv  30285  unelsiga  30738  sibfof  30943  bnj1145  31603  derangenlem  31695  l1cvpat  35128  llnexchb2  35943  hdmapglem7  38003  eel11111  39776  dmrelrnrel  40224  climrec  40628  lptre2pt  40665  0ellimcdiv  40674  iccpartlt  42246