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  7414  marypha1lem  9473  wemaplem3  9588  xpwdomg  9625  pwfseqlem4  10702  wrdind  14760  wrd2ind  14761  sqrt2irr  16285  coprm  16748  oddprmdvds  16941  cyccom  19221  symggen  19488  efgredlemd  19762  efgredlem  19765  efgred  19766  chcoeffeq  22892  nmoleub2lem3  25148  iscmet3  25327  mulsproplem1  28142  axtgcgrid  28471  axtg5seg  28473  axtgbtwnid  28474  wlk1walk  29657  umgr2wlk  29969  frgrnbnb  30312  friendshipgt3  30417  ismntd  32974  archiexdiv  33197  fedgmullem2  33681  unelsiga  34135  sibfof  34342  bnj1145  35007  derangenlem  35176  irrdiff  37327  l1cvpat  39055  llnexchb2  39871  hdmapglem7  41931  eel11111  44743  dmrelrnrel  45231  climrec  45618  lptre2pt  45655  0ellimcdiv  45664  iccpartlt  47411  cycl3grtri  47914