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  7346  marypha1lem  9343  wemaplem3  9460  xpwdomg  9497  pwfseqlem4  10583  wrdind  14682  wrd2ind  14683  sqrt2irr  16214  coprm  16679  oddprmdvds  16872  cyccom  19176  symggen  19443  efgredlemd  19717  efgredlem  19720  efgred  19721  chcoeffeq  22876  nmoleub2lem3  25107  iscmet3  25285  mulsproplem1  28133  axtgcgrid  28556  axtg5seg  28558  axtgbtwnid  28559  wlk1walk  29732  umgr2wlk  30042  frgrnbnb  30388  friendshipgt3  30493  ismntd  33070  archiexdiv  33278  fedgmullem2  33821  unelsiga  34325  sibfof  34531  bnj1145  35182  derangenlem  35406  irrdiff  37693  l1cvpat  39553  llnexchb2  40368  hdmapglem7  42428  eel11111  45173  dmrelrnrel  45678  climrec  46055  lptre2pt  46090  0ellimcdiv  46099  iccpartlt  47906  cycl3grtri  48445