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  7388  marypha1lem  9445  wemaplem3  9562  xpwdomg  9599  pwfseqlem4  10676  wrdind  14740  wrd2ind  14741  sqrt2irr  16267  coprm  16730  oddprmdvds  16923  cyccom  19186  symggen  19451  efgredlemd  19725  efgredlem  19728  efgred  19729  chcoeffeq  22824  nmoleub2lem3  25066  iscmet3  25245  mulsproplem1  28071  axtgcgrid  28442  axtg5seg  28444  axtgbtwnid  28445  wlk1walk  29619  umgr2wlk  29931  frgrnbnb  30274  friendshipgt3  30379  ismntd  32964  archiexdiv  33188  fedgmullem2  33670  unelsiga  34165  sibfof  34372  bnj1145  35024  derangenlem  35193  irrdiff  37344  l1cvpat  39072  llnexchb2  39888  hdmapglem7  41948  eel11111  44747  dmrelrnrel  45250  climrec  45632  lptre2pt  45669  0ellimcdiv  45678  iccpartlt  47438  cycl3grtri  47959