Theorem mt4d 151

Description: Modus tollens deduction. Deduction form of mt4 114. (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 113	. 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  152  fin1a2s  9119  gchinf  9358  pwfseqlem4  9363  isprm2lem  15232  pcfac  15441  prmreclem3  15460  sylow1lem1  17836  irredrmul  18530  mdetunilem9  20245  ioorcl2  23146  itg2gt0  23333  mdegmullem  23642  atom1d  28596  notnotrALT  37756  fourierdlem79  39078