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 ⊢ (𝜑 → 𝜃)

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  7394  marypha1lem  9393  wemaplem3  9510  xpwdomg  9547  pwfseqlem4  10647  wrdind  14759  wrd2ind  14760  sqrt2irr  16305  coprm  16770  oddprmdvds  16963  cyccom  19274  symggen  19540  efgredlemd  19814  efgredlem  19817  efgred  19818  chcoeffeq  23012  nmoleub2lem3  25243  iscmet3  25421  mulsproplem1  28275  axtgcgrid  28698  axtg5seg  28700  axtgbtwnid  28701  wlk1walk  29929  umgr2wlk  30239  frgrnbnb  30585  friendshipgt3  30690  ismntd  33245  archiexdiv  33451  fedgmullem2  33965  unelsiga  34469  sibfof  34675  bnj1145  35326  derangenlem  35596  irrdiff  37893  l1cvpat  39753  llnexchb2  40568  hdmapglem7  42628  eel11111  45358  dmrelrnrel  45869  climrec  46246  lptre2pt  46281  0ellimcdiv  46290  iccpartlt  48097  cycl3grtri  48636