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  7142  marypha1lem  8899  wemaplem3  9014  xpwdomg  9051  wrdind  14086  wrd2ind  14087  sqrt2irr  15604  coprm  16057  oddprmdvds  16241  cyccom  18348  symggen  18600  efgredlemd  18872  efgredlem  18875  efgred  18876  chcoeffeq  21496  nmoleub2lem3  23721  iscmet3  23898  axtgcgrid  26251  axtg5seg  26253  axtgbtwnid  26254  wlk1walk  27422  umgr2wlk  27730  frgrnbnb  28074  friendshipgt3  28179  archiexdiv  30821  fedgmullem2  31028  unelsiga  31395  sibfof  31600  bnj1145  32267  derangenlem  32420  l1cvpat  36192  llnexchb2  37007  hdmapglem7  39067  eel11111  41064  dmrelrnrel  41497  climrec  41891  lptre2pt  41928  0ellimcdiv  41937  iccpartlt  43591