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  7399  marypha1lem  9469  wemaplem3  9584  xpwdomg  9621  wrdind  14725  wrd2ind  14726  sqrt2irr  16246  coprm  16707  oddprmdvds  16900  cyccom  19193  symggen  19464  efgredlemd  19738  efgredlem  19741  efgred  19742  chcoeffeq  22876  nmoleub2lem3  25130  iscmet3  25309  mulsproplem1  28114  axtgcgrid  28387  axtg5seg  28389  axtgbtwnid  28390  wlk1walk  29573  umgr2wlk  29880  frgrnbnb  30223  friendshipgt3  30328  ismntd  32857  archiexdiv  33059  fedgmullem2  33531  unelsiga  33980  sibfof  34187  bnj1145  34851  derangenlem  35012  irrdiff  37046  l1cvpat  38765  llnexchb2  39581  hdmapglem7  41641  eel11111  44436  dmrelrnrel  44869  climrec  45260  lptre2pt  45297  0ellimcdiv  45306  iccpartlt  47032