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  7329  marypha1lem  9317  wemaplem3  9434  xpwdomg  9471  pwfseqlem4  10550  wrdind  14626  wrd2ind  14627  sqrt2irr  16155  coprm  16619  oddprmdvds  16812  cyccom  19113  symggen  19380  efgredlemd  19654  efgredlem  19657  efgred  19658  chcoeffeq  22799  nmoleub2lem3  25040  iscmet3  25218  mulsproplem1  28053  axtgcgrid  28439  axtg5seg  28441  axtgbtwnid  28442  wlk1walk  29615  umgr2wlk  29925  frgrnbnb  30268  friendshipgt3  30373  ismntd  32960  archiexdiv  33154  fedgmullem2  33638  unelsiga  34142  sibfof  34348  bnj1145  35000  derangenlem  35203  irrdiff  37359  l1cvpat  39092  llnexchb2  39907  hdmapglem7  41967  eel11111  44754  dmrelrnrel  45262  climrec  45642  lptre2pt  45677  0ellimcdiv  45686  iccpartlt  47454  cycl3grtri  47977