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  9146  fin1a2s  10336  gchinf  10580  pwfseqlem4  10585  pcfac  16870  prmreclem3  16889  sylow1lem1  19573  irredrmul  20407  mdetunilem9  22585  ioorcl2  25539  itg2gt0  25727  mdegmullem  26043  atom1d  32424  rr-phpd  44636  notnotrALT  44956  fourierdlem79  46613