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

Theorem necon2bd 2839
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 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 241 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 129 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon4bd  2843  necon4d  2847  minel  4066  disjiun  4672  eceqoveq  7895  en3lp  8551  infpssrlem5  9167  nneo  11499  zeo2  11502  sqrt2irr  15023  bezoutr1  15329  coprm  15470  dfphi2  15526  pltirr  17010  oddvdsnn0  18009  psgnodpmr  19984  supnfcls  21871  flimfnfcls  21879  metds0  22700  metdseq0  22704  metnrmlem1a  22708  sineq0  24318  lgsqr  25121  staddi  29233  stadd3i  29235  eulerpartlems  30550  erdszelem8  31306  finminlem  32437  ordcmp  32571  poimirlem18  33557  poimirlem21  33560  cvrnrefN  34887  trlnidatb  35782
  Copyright terms: Public domain W3C validator