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  7119  marypha1lem  8881  wemaplem3  8996  xpwdomg  9033  wrdind  14075  wrd2ind  14076  sqrt2irr  15594  coprm  16045  oddprmdvds  16229  cyccom  18338  symggen  18590  efgredlemd  18862  efgredlem  18865  efgred  18866  chcoeffeq  21491  nmoleub2lem3  23720  iscmet3  23897  axtgcgrid  26257  axtg5seg  26259  axtgbtwnid  26260  wlk1walk  27428  umgr2wlk  27735  frgrnbnb  28078  friendshipgt3  28183  ismntd  30692  archiexdiv  30869  fedgmullem2  31114  unelsiga  31503  sibfof  31708  bnj1145  32375  derangenlem  32531  irrdiff  34740  l1cvpat  36350  llnexchb2  37165  hdmapglem7  39225  eel11111  41429  dmrelrnrel  41856  climrec  42245  lptre2pt  42282  0ellimcdiv  42291  iccpartlt  43941