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  9278  phpeqdOLD  9288  fin1a2s  10483  gchinf  10726  pwfseqlem4  10731  pcfac  16946  prmreclem3  16965  sylow1lem1  19640  irredrmul  20453  mdetunilem9  22647  ioorcl2  25626  itg2gt0  25815  mdegmullem  26137  atom1d  32385  rr-phpd  44172  notnotrALT  44500  fourierdlem79  46106