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  7431  marypha1lem  9502  wemaplem3  9617  xpwdomg  9654  pwfseqlem4  10731  wrdind  14770  wrd2ind  14771  sqrt2irr  16297  coprm  16758  oddprmdvds  16950  cyccom  19243  symggen  19512  efgredlemd  19786  efgredlem  19789  efgred  19790  chcoeffeq  22913  nmoleub2lem3  25167  iscmet3  25346  mulsproplem1  28160  axtgcgrid  28489  axtg5seg  28491  axtgbtwnid  28492  wlk1walk  29675  umgr2wlk  29982  frgrnbnb  30325  friendshipgt3  30430  ismntd  32957  archiexdiv  33170  fedgmullem2  33643  unelsiga  34098  sibfof  34305  bnj1145  34969  derangenlem  35139  irrdiff  37292  l1cvpat  39010  llnexchb2  39826  hdmapglem7  41886  eel11111  44694  dmrelrnrel  45133  climrec  45524  lptre2pt  45561  0ellimcdiv  45570  iccpartlt  47298