Theorem mp2d 50

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 45	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	1, 4	mpd 16	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  riotaeqimp  7426  marypha1lem  9452  wemaplem3  9569  xpwdomg  9606  pwfseqlem4  10774  wrdind  14899  wrd2ind  14900  sqrt2irr  16446  coprm  16916  oddprmdvds  17110  cyccom  19447  symggen  19714  efgredlemd  19988  efgredlem  19991  efgred  19992  chcoeffeq  23234  nmoleub2lem3  25466  iscmet3  25644  mulsproplem1  28532  axtgcgrid  28955  axtg5seg  28957  axtgbtwnid  28958  wlk1walk  30249  umgr2wlk  30568  frgrnbnb  30924  friendshipgt3  31029  ismntd  33615  archiexdiv  33821  fedgmullem2  34332  unelsiga  34836  sibfof  35042  bnj1145  35693  derangenlem  36103  irrdiff  38439  l1cvpat  40303  llnexchb2  41118  hdmapglem7  43178  eel11111  45896  dmrelrnrel  46444  climrec  46820  lptre2pt  46855  0ellimcdiv  46864  iccpartlt  48711  cycl3grtri  49250