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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  432  ceqsalt  2848  rspcimdv  2930  fvimacnv  5824  riotass2  6067  pr2ne  7538  0mnnnnn0  9597  caucvgre  11749  climcn1  12076  climcn2  12077  gcdaddm  12763  dvdsgcd  12791  coprmgcdb  12868  nprm  12903  pcqmul  13084  grpid  13846  uniopn  15104  metcnp3  15614  cncfco  15694  eupth2fi  16732