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  7336  marypha1lem  9342  wemaplem3  9459  xpwdomg  9496  pwfseqlem4  10575  wrdind  14646  wrd2ind  14647  sqrt2irr  16176  coprm  16640  oddprmdvds  16833  cyccom  19100  symggen  19367  efgredlemd  19641  efgredlem  19644  efgred  19645  chcoeffeq  22789  nmoleub2lem3  25031  iscmet3  25209  mulsproplem1  28042  axtgcgrid  28426  axtg5seg  28428  axtgbtwnid  28429  wlk1walk  29602  umgr2wlk  29912  frgrnbnb  30255  friendshipgt3  30360  ismntd  32939  archiexdiv  33142  fedgmullem2  33602  unelsiga  34100  sibfof  34307  bnj1145  34959  derangenlem  35143  irrdiff  37299  l1cvpat  39032  llnexchb2  39848  hdmapglem7  41908  eel11111  44696  dmrelrnrel  45204  climrec  45585  lptre2pt  45622  0ellimcdiv  45631  iccpartlt  47409  cycl3grtri  47932