Theorem mt4d 117

Description: Modus tollens deduction. Deduction form of mt4 116. (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 115	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mt4i  118  pm2.18d  127  phpeqd  8700  fin1a2s  9830  gchinf  10073  pwfseqlem4  10078  pcfac  16229  prmreclem3  16248  sylow1lem1  18717  irredrmul  19451  mdetunilem9  21223  ioorcl2  24167  itg2gt0  24355  mdegmullem  24666  atom1d  30124  rr-phpd  40555  notnotrALT  40856  fourierdlem79  42464