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  7395  marypha1lem  9409  wemaplem3  9526  xpwdomg  9563  pwfseqlem4  10728  wrdind  14851  wrd2ind  14852  sqrt2irr  16397  coprm  16867  oddprmdvds  17061  cyccom  19398  symggen  19664  efgredlemd  19938  efgredlem  19941  efgred  19942  chcoeffeq  23184  nmoleub2lem3  25416  iscmet3  25594  mulsproplem1  28484  axtgcgrid  28907  axtg5seg  28909  axtgbtwnid  28910  wlk1walk  30201  umgr2wlk  30520  frgrnbnb  30876  friendshipgt3  30981  ismntd  33527  archiexdiv  33733  fedgmullem2  34244  unelsiga  34748  sibfof  34955  bnj1145  35606  derangenlem  35905  irrdiff  38215  l1cvpat  40079  llnexchb2  40894  hdmapglem7  42954  eel11111  45664  dmrelrnrel  46182  climrec  46559  lptre2pt  46594  0ellimcdiv  46603  iccpartlt  48450  cycl3grtri  48989