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  7400  marypha1lem  9407  wemaplem3  9524  xpwdomg  9561  pwfseqlem4  10675  wrdind  14795  wrd2ind  14796  sqrt2irr  16343  coprm  16808  oddprmdvds  17001  cyccom  19337  symggen  19603  efgredlemd  19877  efgredlem  19880  efgred  19881  chcoeffeq  23117  nmoleub2lem3  25349  iscmet3  25527  mulsproplem1  28389  axtgcgrid  28812  axtg5seg  28814  axtgbtwnid  28815  wlk1walk  30106  umgr2wlk  30425  frgrnbnb  30781  friendshipgt3  30886  ismntd  33432  archiexdiv  33638  fedgmullem2  34148  unelsiga  34652  sibfof  34859  bnj1145  35510  derangenlem  35758  irrdiff  38086  l1cvpat  39935  llnexchb2  40750  hdmapglem7  42810  eel11111  45553  dmrelrnrel  46064  climrec  46441  lptre2pt  46476  0ellimcdiv  46485  iccpartlt  48332  cycl3grtri  48871