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 252 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 136 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  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 208  df-ne 3017
This theorem is referenced by:  necon4bd  3036  necon4d  3040  minel  4413  disjiun  5045  eceqoveq  8392  en3lp  9066  infpssrlem5  9718  nneo  12055  zeo2  12058  sqrt2irr  15592  bezoutr1  15903  coprm  16045  dfphi2  16101  pltirr  17563  oddvdsnn0  18603  psgnodpmr  20664  supnfcls  22558  flimfnfcls  22566  metds0  23387  metdseq0  23391  metnrmlem1a  23395  sineq0  25038  lgsqr  25855  staddi  29951  stadd3i  29953  eulerpartlems  31518  erdszelem8  32343  finminlem  33564  ordcmp  33693  poimirlem18  34792  poimirlem21  34795  cvrnrefN  36300  trlnidatb  37195
  Copyright terms: Public domain W3C validator