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  7397  marypha1lem  9448  wemaplem3  9563  xpwdomg  9600  wrdind  14696  wrd2ind  14697  sqrt2irr  16217  coprm  16673  oddprmdvds  16863  cyccom  19149  symggen  19416  efgredlemd  19690  efgredlem  19693  efgred  19694  chcoeffeq  22775  nmoleub2lem3  25029  iscmet3  25208  mulsproplem1  28003  axtgcgrid  28254  axtg5seg  28256  axtgbtwnid  28257  wlk1walk  29440  umgr2wlk  29747  frgrnbnb  30090  friendshipgt3  30195  ismntd  32693  archiexdiv  32876  fedgmullem2  33260  unelsiga  33689  sibfof  33896  bnj1145  34560  derangenlem  34717  irrdiff  36741  l1cvpat  38463  llnexchb2  39279  hdmapglem7  41339  eel11111  44085  dmrelrnrel  44522  climrec  44914  lptre2pt  44951  0ellimcdiv  44960  iccpartlt  46687