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  7413  marypha1lem  9470  wemaplem3  9585  xpwdomg  9622  pwfseqlem4  10699  wrdind  14756  wrd2ind  14757  sqrt2irr  16281  coprm  16744  oddprmdvds  16936  cyccom  19233  symggen  19502  efgredlemd  19776  efgredlem  19779  efgred  19780  chcoeffeq  22907  nmoleub2lem3  25161  iscmet3  25340  mulsproplem1  28156  axtgcgrid  28485  axtg5seg  28487  axtgbtwnid  28488  wlk1walk  29671  umgr2wlk  29978  frgrnbnb  30321  friendshipgt3  30426  ismntd  32958  archiexdiv  33179  fedgmullem2  33657  unelsiga  34114  sibfof  34321  bnj1145  34985  derangenlem  35155  irrdiff  37308  l1cvpat  39035  llnexchb2  39851  hdmapglem7  41911  eel11111  44720  dmrelrnrel  45168  climrec  45558  lptre2pt  45595  0ellimcdiv  45604  iccpartlt  47348