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  7400  marypha1lem  9456  wemaplem3  9571  xpwdomg  9608  wrdind  14704  wrd2ind  14705  sqrt2irr  16225  coprm  16681  oddprmdvds  16871  cyccom  19162  symggen  19429  efgredlemd  19703  efgredlem  19706  efgred  19707  chcoeffeq  22818  nmoleub2lem3  25072  iscmet3  25251  mulsproplem1  28050  axtgcgrid  28323  axtg5seg  28325  axtgbtwnid  28326  wlk1walk  29509  umgr2wlk  29816  frgrnbnb  30159  friendshipgt3  30264  ismntd  32768  archiexdiv  32955  fedgmullem2  33398  unelsiga  33823  sibfof  34030  bnj1145  34694  derangenlem  34851  irrdiff  36875  l1cvpat  38595  llnexchb2  39411  hdmapglem7  41471  eel11111  44227  dmrelrnrel  44663  climrec  45054  lptre2pt  45091  0ellimcdiv  45100  iccpartlt  46827