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

Theorem necon2bd 2976
Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon2bd.1 (𝜑 → (𝜓𝐴𝐵))
Assertion
Ref Expression
necon2bd (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Proof of Theorem necon2bd
StepHypRef Expression
1 necon2bd.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
2 df-ne 2961 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2imbitrdi 254 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 135 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1563  wne 2960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-ne 2961
This theorem is referenced by:  necon4bd  2980  necon4d  2984  minel  4423  disjiun  5092  eceqoveq  8808  en3lp  9571  infpssrlem5  10279  nneo  12668  zeo2  12671  sqrt2irr  16293  bezoutr1  16615  coprm  16758  dfphi2  16821  pltirr  18377  oddvdsnn0  19602  psgnodpmr  21697  supnfcls  24134  flimfnfcls  24142  metds0  24965  metdseq0  24969  metnrmlem1a  24973  sineq0  26643  lgsqr  27469  staddi  32503  stadd3i  32505  eulerpartlems  34662  erdszelem8  35556  finminlem  36686  ordcmp  36815  poimirlem18  38144  poimirlem21  38147  cvrnrefN  39913  trlnidatb  40808  flt4lem2  43236
  Copyright terms: Public domain W3C validator