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  9227  fin1a2s  10492  gchinf  10742  pwfseqlem4  10747  pcfac  17077  prmreclem3  17096  sylow1lem1  19812  irredrmul  20657  mdetunilem9  22935  ioorcl2  25893  itg2gt0  26081  mdegmullem  26396  atom1d  32955  rr-phpd  45249  notnotrALT  45554  fourierdlem79  47237