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 ⊢ (𝜑 → 𝜃)

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  7395  marypha1lem  9394  wemaplem3  9511  xpwdomg  9548  pwfseqlem4  10648  wrdind  14761  wrd2ind  14762  sqrt2irr  16306  coprm  16771  oddprmdvds  16964  cyccom  19275  symggen  19541  efgredlemd  19815  efgredlem  19818  efgred  19819  chcoeffeq  23024  nmoleub2lem3  25255  iscmet3  25433  mulsproplem1  28287  axtgcgrid  28710  axtg5seg  28712  axtgbtwnid  28713  wlk1walk  29966  umgr2wlk  30276  frgrnbnb  30622  friendshipgt3  30727  ismntd  33282  archiexdiv  33488  fedgmullem2  33998  unelsiga  34502  sibfof  34708  bnj1145  35359  derangenlem  35641  irrdiff  37948  l1cvpat  39806  llnexchb2  40621  hdmapglem7  42681  eel11111  45411  dmrelrnrel  45922  climrec  46299  lptre2pt  46334  0ellimcdiv  46343  iccpartlt  48150  cycl3grtri  48689