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  9428  gchinf  9671  pwfseqlem4  9676  pcfac  15805  prmreclem3  15824  sylow1lem1  18213  irredrmul  18907  mdetunilem9  20628  ioorcl2  23540  itg2gt0  23726  mdegmullem  24037  atom1d  29521  notnotrALT  39237  fourierdlem79  40905
  Copyright terms: Public domain W3C validator