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

Theorem mt4d 152
Description: Modus tollens deduction. Deduction form of mt4 115. (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 114 . 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  153  fin1a2s  9221  gchinf  9464  pwfseqlem4  9469  isprm2lem  15375  pcfac  15584  prmreclem3  15603  sylow1lem1  17994  irredrmul  18688  mdetunilem9  20407  ioorcl2  23321  itg2gt0  23508  mdegmullem  23819  atom1d  29182  notnotrALT  38555  fourierdlem79  40165
  Copyright terms: Public domain W3C validator