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  7373  marypha1lem  9391  wemaplem3  9508  xpwdomg  9545  pwfseqlem4  10622  wrdind  14694  wrd2ind  14695  sqrt2irr  16224  coprm  16688  oddprmdvds  16881  cyccom  19142  symggen  19407  efgredlemd  19681  efgredlem  19684  efgred  19685  chcoeffeq  22780  nmoleub2lem3  25022  iscmet3  25200  mulsproplem1  28026  axtgcgrid  28397  axtg5seg  28399  axtgbtwnid  28400  wlk1walk  29574  umgr2wlk  29886  frgrnbnb  30229  friendshipgt3  30334  ismntd  32917  archiexdiv  33151  fedgmullem2  33633  unelsiga  34131  sibfof  34338  bnj1145  34990  derangenlem  35165  irrdiff  37321  l1cvpat  39054  llnexchb2  39870  hdmapglem7  41930  eel11111  44719  dmrelrnrel  45227  climrec  45608  lptre2pt  45645  0ellimcdiv  45654  iccpartlt  47429  cycl3grtri  47950