Theorem mp2d 49

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 44	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	1, 4	mpd 15	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  7335  marypha1lem  9324  wemaplem3  9441  xpwdomg  9478  pwfseqlem4  10560  wrdind  14631  wrd2ind  14632  sqrt2irr  16160  coprm  16624  oddprmdvds  16817  cyccom  19117  symggen  19384  efgredlemd  19658  efgredlem  19661  efgred  19662  chcoeffeq  22802  nmoleub2lem3  25043  iscmet3  25221  mulsproplem1  28056  axtgcgrid  28442  axtg5seg  28444  axtgbtwnid  28445  wlk1walk  29619  umgr2wlk  29929  frgrnbnb  30275  friendshipgt3  30380  ismntd  32972  archiexdiv  33166  fedgmullem2  33664  unelsiga  34168  sibfof  34374  bnj1145  35026  derangenlem  35236  irrdiff  37391  l1cvpat  39173  llnexchb2  39988  hdmapglem7  42048  eel11111  44839  dmrelrnrel  45347  climrec  45727  lptre2pt  45762  0ellimcdiv  45771  iccpartlt  47548  cycl3grtri  48071