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

Theorem necon2bd 2797
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 2781 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 239 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 127 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon4bd  2801  necon4d  2805  minel  3984  disjiun  4567  eceqoveq  7717  en3lp  8373  infpssrlem5  8989  nneo  11295  zeo2  11298  sqrt2irr  14765  bezoutr1  15068  coprm  15209  dfphi2  15265  pltirr  16734  oddvdsnn0  17734  psgnodpmr  19702  supnfcls  21581  flimfnfcls  21589  metds0  22408  metdseq0  22412  metnrmlem1a  22416  sineq0  24021  lgsqr  24820  staddi  28282  stadd3i  28284  eulerpartlems  29542  erdszelem8  30227  finminlem  31275  ordcmp  31409  poimirlem18  32380  poimirlem21  32383  cvrnrefN  33370  trlnidatb  34265
  Copyright terms: Public domain W3C validator