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  7343  marypha1lem  9339  wemaplem3  9456  xpwdomg  9493  pwfseqlem4  10576  wrdind  14675  wrd2ind  14676  sqrt2irr  16207  coprm  16672  oddprmdvds  16865  cyccom  19169  symggen  19436  efgredlemd  19710  efgredlem  19713  efgred  19714  chcoeffeq  22861  nmoleub2lem3  25092  iscmet3  25270  mulsproplem1  28122  axtgcgrid  28545  axtg5seg  28547  axtgbtwnid  28548  wlk1walk  29722  umgr2wlk  30032  frgrnbnb  30378  friendshipgt3  30483  ismntd  33059  archiexdiv  33266  fedgmullem2  33790  unelsiga  34294  sibfof  34500  bnj1145  35151  derangenlem  35369  irrdiff  37656  l1cvpat  39514  llnexchb2  40329  hdmapglem7  42389  eel11111  45167  dmrelrnrel  45673  climrec  46051  lptre2pt  46086  0ellimcdiv  46095  iccpartlt  47896  cycl3grtri  48435