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  7341  marypha1lem  9336  wemaplem3  9453  xpwdomg  9490  pwfseqlem4  10573  wrdind  14645  wrd2ind  14646  sqrt2irr  16174  coprm  16638  oddprmdvds  16831  cyccom  19132  symggen  19399  efgredlemd  19673  efgredlem  19676  efgred  19677  chcoeffeq  22830  nmoleub2lem3  25071  iscmet3  25249  mulsproplem1  28112  axtgcgrid  28535  axtg5seg  28537  axtgbtwnid  28538  wlk1walk  29712  umgr2wlk  30022  frgrnbnb  30368  friendshipgt3  30473  ismntd  33066  archiexdiv  33272  fedgmullem2  33787  unelsiga  34291  sibfof  34497  bnj1145  35149  derangenlem  35365  irrdiff  37527  l1cvpat  39310  llnexchb2  40125  hdmapglem7  42185  eel11111  44959  dmrelrnrel  45466  climrec  45845  lptre2pt  45880  0ellimcdiv  45889  iccpartlt  47666  cycl3grtri  48189