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  7383  marypha1lem  9381  wemaplem3  9498  xpwdomg  9535  pwfseqlem4  10635  wrdind  14749  wrd2ind  14750  sqrt2irr  16295  coprm  16760  oddprmdvds  16953  cyccom  19265  symggen  19531  efgredlemd  19805  efgredlem  19808  efgred  19809  chcoeffeq  23004  nmoleub2lem3  25235  iscmet3  25413  mulsproplem1  28267  axtgcgrid  28690  axtg5seg  28692  axtgbtwnid  28693  wlk1walk  29897  umgr2wlk  30207  frgrnbnb  30553  friendshipgt3  30658  ismntd  33217  archiexdiv  33423  fedgmullem2  33937  unelsiga  34441  sibfof  34647  bnj1145  35298  derangenlem  35534  irrdiff  37830  l1cvpat  39690  llnexchb2  40505  hdmapglem7  42565  eel11111  45296  dmrelrnrel  45800  climrec  46177  lptre2pt  46212  0ellimcdiv  46221  iccpartlt  48028  cycl3grtri  48567