Theorem mp2d 50

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 45	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
5	1, 4	mpd 16	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  riotaeqimp  7403  marypha1lem  9428  wemaplem3  9545  xpwdomg  9582  pwfseqlem4  10750  wrdind  14875  wrd2ind  14876  sqrt2irr  16422  coprm  16892  oddprmdvds  17086  cyccom  19423  symggen  19689  efgredlemd  19963  efgredlem  19966  efgred  19967  chcoeffeq  23209  nmoleub2lem3  25441  iscmet3  25619  mulsproplem1  28507  axtgcgrid  28930  axtg5seg  28932  axtgbtwnid  28933  wlk1walk  30224  umgr2wlk  30543  frgrnbnb  30899  friendshipgt3  31004  ismntd  33591  archiexdiv  33797  fedgmullem2  34308  unelsiga  34812  sibfof  35018  bnj1145  35669  derangenlem  36022  irrdiff  38340  l1cvpat  40204  llnexchb2  41019  hdmapglem7  43079  eel11111  45798  dmrelrnrel  46332  climrec  46708  lptre2pt  46743  0ellimcdiv  46752  iccpartlt  48599  cycl3grtri  49138