Theorem mp2d 47

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 43	. 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:  marypha1lem  8222  wemaplem3  8336  xpwdomg  8373  wrdind  13328  wrd2ind  13329  sqrt2irr  14817  coprm  15261  oddprmdvds  15445  symggen  17713  efgredlemd  17980  efgredlem  17983  efgred  17984  chcoeffeq  20510  nmoleub2lem3  22723  iscmet3  22899  axtgcgrid  25162  axtg5seg  25164  axtgbtwnid  25165  frgranbnb  26547  vdgfrgragt2  26554  friendshipgt3  26648  archiexdiv  29075  unelsiga  29524  sibfof  29729  bnj1145  30315  derangenlem  30407  l1cvpat  33359  llnexchb2  34173  hdmapglem7  36239  eel11111  37971  climrec  38670  lptre2pt  38707  0ellimcdiv  38716  iccpartlt  39962  riotaeqimp  40338  1wlk1walk  40843  umgr2wlk  41156  frgrnbnb  41463  av-friendshipgt3  41552