Theorem mt4d 118

Description: Modus tollens deduction. Deduction form of mt4 117. (Contributed by NM, 9-Jun-2006.)

Hypotheses

Ref	Expression
mt4d.1	⊢ (𝜑 → 𝜓)
mt4d.2	⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Assertion

Ref	Expression
mt4d	⊢ (𝜑 → 𝜒)

Proof of Theorem mt4d

Step	Hyp	Ref	Expression
1		mt4d.1	. 2 ⊢ (𝜑 → 𝜓)
2		mt4d.2	. . 3 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

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

This theorem is used by:  mt4i  119  pm2.18d  128  phpeqd  9255  fin1a2s  10519  gchinf  10769  pwfseqlem4  10774  pcfac  17106  prmreclem3  17125  sylow1lem1  19842  irredrmul  20687  mdetunilem9  22965  ioorcl2  25923  itg2gt0  26111  mdegmullem  26426  atom1d  32985  rr-phpd  45399  notnotrALT  45703  fourierdlem79  47400