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 ⊢ (𝜑 → 𝜒)

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  119  pm2.18d  128  phpeqd  9195  fin1a2s  10397  gchinf  10641  pwfseqlem4  10646  pcfac  16958  prmreclem3  16977  sylow1lem1  19667  irredrmul  20508  mdetunilem9  22756  ioorcl2  25710  itg2gt0  25898  mdegmullem  26214  atom1d  32671  rr-phpd  44903  notnotrALT  45208  fourierdlem79  46869