Theorem mpid 42

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

Hypotheses

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

Assertion

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

Proof of Theorem mpid

Step	Hyp	Ref	Expression
1		mpid.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	a1d 22	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		mpid.2	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	2, 3	mpdd 41	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:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  428  ceqsalt  2842  rspcimdv  2924  fvimacnv  5795  riotass2  6034  pr2ne  7491  0mnnnnn0  9533  caucvgre  11674  climcn1  12001  climcn2  12002  gcdaddm  12688  dvdsgcd  12716  coprmgcdb  12793  nprm  12828  pcqmul  13009  grpid  13773  uniopn  14915  metcnp3  15425  cncfco  15505  eupth2fi  16523