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

Theorem necon2bd 2959
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 2944 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 250 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 134 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2943
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 206  df-ne 2944
This theorem is referenced by:  necon4bd  2963  necon4d  2967  minel  4399  disjiun  5061  eceqoveq  8611  en3lp  9372  infpssrlem5  10063  nneo  12404  zeo2  12407  sqrt2irr  15958  bezoutr1  16274  coprm  16416  dfphi2  16475  pltirr  18053  oddvdsnn0  19152  psgnodpmr  20795  supnfcls  23171  flimfnfcls  23179  metds0  24013  metdseq0  24017  metnrmlem1a  24021  sineq0  25680  lgsqr  26499  staddi  30608  stadd3i  30610  eulerpartlems  32327  erdszelem8  33160  finminlem  34507  ordcmp  34636  poimirlem18  35795  poimirlem21  35798  cvrnrefN  37296  trlnidatb  38191  flt4lem2  40484
  Copyright terms: Public domain W3C validator