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  9209  fin1a2s  10419  gchinf  10669  pwfseqlem4  10674  pcfac  16995  prmreclem3  17014  sylow1lem1  19729  irredrmul  20572  mdetunilem9  22846  ioorcl2  25804  itg2gt0  25992  mdegmullem  26308  atom1d  32835  rr-phpd  45049  notnotrALT  45354  fourierdlem79  47015