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  7329  marypha1lem  9317  wemaplem3  9434  xpwdomg  9471  pwfseqlem4  10553  wrdind  14629  wrd2ind  14630  sqrt2irr  16158  coprm  16622  oddprmdvds  16815  cyccom  19115  symggen  19382  efgredlemd  19656  efgredlem  19659  efgred  19660  chcoeffeq  22801  nmoleub2lem3  25042  iscmet3  25220  mulsproplem1  28055  axtgcgrid  28441  axtg5seg  28443  axtgbtwnid  28444  wlk1walk  29617  umgr2wlk  29927  frgrnbnb  30273  friendshipgt3  30378  ismntd  32965  archiexdiv  33159  fedgmullem2  33643  unelsiga  34147  sibfof  34353  bnj1145  35005  derangenlem  35215  irrdiff  37370  l1cvpat  39152  llnexchb2  39967  hdmapglem7  42027  eel11111  44814  dmrelrnrel  45322  climrec  45702  lptre2pt  45737  0ellimcdiv  45746  iccpartlt  47523  cycl3grtri  48046