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  5093  eceqoveq  8808  en3lp  9571  infpssrlem5  10279  nneo  12671  zeo2  12674  sqrt2irr  16295  bezoutr1  16617  coprm  16760  dfphi2  16823  pltirr  18379  oddvdsnn0  19605  psgnodpmr  21700  supnfcls  24138  flimfnfcls  24146  metds0  24969  metdseq0  24973  metnrmlem1a  24977  sineq0  26647  lgsqr  27473  staddi  32507  stadd3i  32509  eulerpartlems  34667  erdszelem8  35561  finminlem  36691  ordcmp  36820  poimirlem18  38149  poimirlem21  38152  cvrnrefN  39918  trlnidatb  40813  flt4lem2  43241
  Copyright terms: Public domain W3C validator