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

Theorem necon2bd 2960
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 2945 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2syl6ib 251 . 2 (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
43con2d 134 1 (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2944
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 206  df-ne 2945
This theorem is referenced by:  necon4bd  2964  necon4d  2968  minel  4430  disjiun  5097  eceqoveq  8768  en3lp  9557  infpssrlem5  10250  nneo  12594  zeo2  12597  sqrt2irr  16138  bezoutr1  16452  coprm  16594  dfphi2  16653  pltirr  18231  oddvdsnn0  19333  psgnodpmr  21010  supnfcls  23387  flimfnfcls  23395  metds0  24229  metdseq0  24233  metnrmlem1a  24237  sineq0  25896  lgsqr  26715  staddi  31230  stadd3i  31232  eulerpartlems  33000  erdszelem8  33832  finminlem  34819  ordcmp  34948  poimirlem18  36125  poimirlem21  36128  cvrnrefN  37773  trlnidatb  38669  flt4lem2  41014
  Copyright terms: Public domain W3C validator