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  7351  marypha1lem  9348  wemaplem3  9465  xpwdomg  9502  pwfseqlem4  10585  wrdind  14657  wrd2ind  14658  sqrt2irr  16186  coprm  16650  oddprmdvds  16843  cyccom  19144  symggen  19411  efgredlemd  19685  efgredlem  19688  efgred  19689  chcoeffeq  22842  nmoleub2lem3  25083  iscmet3  25261  mulsproplem1  28124  axtgcgrid  28547  axtg5seg  28549  axtgbtwnid  28550  wlk1walk  29724  umgr2wlk  30034  frgrnbnb  30380  friendshipgt3  30485  ismntd  33076  archiexdiv  33283  fedgmullem2  33807  unelsiga  34311  sibfof  34517  bnj1145  35168  derangenlem  35384  irrdiff  37575  l1cvpat  39424  llnexchb2  40239  hdmapglem7  42299  eel11111  45072  dmrelrnrel  45578  climrec  45957  lptre2pt  45992  0ellimcdiv  46001  iccpartlt  47778  cycl3grtri  48301