MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mt4d Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mt4d.1 . 2 (𝜑𝜓)
2 mt4d.2 . . 3 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 115 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
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  9155  phpeqdOLD  9165  fin1a2s  10346  gchinf  10589  pwfseqlem4  10594  pcfac  16763  prmreclem3  16782  sylow1lem1  19371  irredrmul  20121  mdetunilem9  21953  ioorcl2  24920  itg2gt0  25109  mdegmullem  25427  atom1d  31181  rr-phpd  42425  notnotrALT  42753  fourierdlem79  44358
  Copyright terms: Public domain W3C validator