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

Theorem necon2bd 2950
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 2935 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 254 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 136 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2934
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 2935
This theorem is referenced by:  necon4bd  2954  necon4d  2958  minel  4355  disjiun  5017  eceqoveq  8433  en3lp  9150  infpssrlem5  9807  nneo  12147  zeo2  12150  sqrt2irr  15694  bezoutr1  16010  coprm  16152  dfphi2  16211  pltirr  17689  oddvdsnn0  18790  psgnodpmr  20406  supnfcls  22771  flimfnfcls  22779  metds0  23602  metdseq0  23606  metnrmlem1a  23610  sineq0  25268  lgsqr  26087  staddi  30181  stadd3i  30183  eulerpartlems  31897  erdszelem8  32731  finminlem  34150  ordcmp  34279  poimirlem18  35438  poimirlem21  35441  cvrnrefN  36939  trlnidatb  37834  flt4lem2  40076
  Copyright terms: Public domain W3C validator