Theorem mpdd 41

Description: A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mpdd.1	⊢ (𝜑 → (𝜓 → 𝜒))
mpdd.2	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
mpdd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpdd

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mpdd.2	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	a2d 26	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 13	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:  mpid  42  mpdi  43  syld  45  syl6c  66  mpteqb  5746  oprabid  6060  nnmordi  6727  nnmord  6728  brecop  6837  findcard2  7121  findcard2s  7122  ordiso2  7277  zindd  9642  ccatopth2  11347  cau3lem  11737  climcau  11970  dvdsabseq  12471  znrrg  14739  metrest  15300  bj-charfunr  16509