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  7350  marypha1lem  9346  wemaplem3  9463  xpwdomg  9500  pwfseqlem4  10585  wrdind  14684  wrd2ind  14685  sqrt2irr  16216  coprm  16681  oddprmdvds  16874  cyccom  19178  symggen  19445  efgredlemd  19719  efgredlem  19722  efgred  19723  chcoeffeq  22851  nmoleub2lem3  25082  iscmet3  25260  mulsproplem1  28108  axtgcgrid  28531  axtg5seg  28533  axtgbtwnid  28534  wlk1walk  29707  umgr2wlk  30017  frgrnbnb  30363  friendshipgt3  30468  ismntd  33044  archiexdiv  33251  fedgmullem2  33774  unelsiga  34278  sibfof  34484  bnj1145  35135  derangenlem  35353  irrdiff  37640  l1cvpat  39500  llnexchb2  40315  hdmapglem7  42375  eel11111  45149  dmrelrnrel  45655  climrec  46033  lptre2pt  46068  0ellimcdiv  46077  iccpartlt  47884  cycl3grtri  48423