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  9205  fin1a2s  10464  gchinf  10714  pwfseqlem4  10719  pcfac  17039  prmreclem3  17058  sylow1lem1  19774  irredrmul  20619  mdetunilem9  22897  ioorcl2  25855  itg2gt0  26043  mdegmullem  26358  atom1d  32889  rr-phpd  45151  notnotrALT  45456  fourierdlem79  47117