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

Theorem necon2bd 3032
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 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 253 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 136 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wne 3016
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 209  df-ne 3017
This theorem is referenced by:  necon4bd  3036  necon4d  3040  minel  4414  disjiun  5052  eceqoveq  8401  en3lp  9076  infpssrlem5  9728  nneo  12065  zeo2  12068  sqrt2irr  15601  bezoutr1  15912  coprm  16054  dfphi2  16110  pltirr  17572  oddvdsnn0  18671  psgnodpmr  20733  supnfcls  22627  flimfnfcls  22635  metds0  23457  metdseq0  23461  metnrmlem1a  23465  sineq0  25108  lgsqr  25926  staddi  30022  stadd3i  30024  eulerpartlems  31618  erdszelem8  32445  finminlem  33666  ordcmp  33795  poimirlem18  34909  poimirlem21  34912  cvrnrefN  36417  trlnidatb  37312
  Copyright terms: Public domain W3C validator