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  7375  marypha1lem  9376  wemaplem3  9493  xpwdomg  9530  pwfseqlem4  10617  wrdind  14732  wrd2ind  14733  sqrt2irr  16264  coprm  16729  oddprmdvds  16922  cyccom  19227  symggen  19493  efgredlemd  19767  efgredlem  19770  efgred  19771  chcoeffeq  22926  nmoleub2lem3  25157  iscmet3  25335  mulsproplem1  28186  axtgcgrid  28609  axtg5seg  28611  axtgbtwnid  28612  wlk1walk  29785  umgr2wlk  30095  frgrnbnb  30441  friendshipgt3  30546  ismntd  33123  archiexdiv  33331  fedgmullem2  33888  unelsiga  34392  sibfof  34598  bnj1145  35252  derangenlem  35485  irrdiff  37782  l1cvpat  39642  llnexchb2  40457  hdmapglem7  42517  eel11111  45262  dmrelrnrel  45766  climrec  46143  lptre2pt  46178  0ellimcdiv  46187  iccpartlt  47994  cycl3grtri  48533