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  7406  marypha1lem  9403  wemaplem3  9520  xpwdomg  9557  pwfseqlem4  10665  wrdind  14783  wrd2ind  14784  sqrt2irr  16330  coprm  16795  oddprmdvds  16988  cyccom  19305  symggen  19571  efgredlemd  19845  efgredlem  19848  efgred  19849  chcoeffeq  23080  nmoleub2lem3  25311  iscmet3  25489  mulsproplem1  28346  axtgcgrid  28769  axtg5seg  28771  axtgbtwnid  28772  wlk1walk  30025  umgr2wlk  30335  frgrnbnb  30681  friendshipgt3  30786  ismntd  33335  archiexdiv  33541  fedgmullem2  34051  unelsiga  34555  sibfof  34762  bnj1145  35413  derangenlem  35684  irrdiff  38011  l1cvpat  39869  llnexchb2  40684  hdmapglem7  42744  eel11111  45472  dmrelrnrel  45983  climrec  46360  lptre2pt  46395  0ellimcdiv  46404  iccpartlt  48214  cycl3grtri  48753