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  7370  marypha1lem  9384  wemaplem3  9501  xpwdomg  9538  pwfseqlem4  10615  wrdind  14687  wrd2ind  14688  sqrt2irr  16217  coprm  16681  oddprmdvds  16874  cyccom  19135  symggen  19400  efgredlemd  19674  efgredlem  19677  efgred  19678  chcoeffeq  22773  nmoleub2lem3  25015  iscmet3  25193  mulsproplem1  28019  axtgcgrid  28390  axtg5seg  28392  axtgbtwnid  28393  wlk1walk  29567  umgr2wlk  29879  frgrnbnb  30222  friendshipgt3  30327  ismntd  32910  archiexdiv  33144  fedgmullem2  33626  unelsiga  34124  sibfof  34331  bnj1145  34983  derangenlem  35158  irrdiff  37314  l1cvpat  39047  llnexchb2  39863  hdmapglem7  41923  eel11111  44712  dmrelrnrel  45220  climrec  45601  lptre2pt  45638  0ellimcdiv  45647  iccpartlt  47425  cycl3grtri  47946