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

Theorem necon3i 2814
 Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon3i.1 (𝐴 = 𝐵𝐶 = 𝐷)
Assertion
Ref Expression
necon3i (𝐶𝐷𝐴𝐵)

Proof of Theorem necon3i
StepHypRef Expression
1 necon3i.1 . . 3 (𝐴 = 𝐵𝐶 = 𝐷)
21necon3ai 2807 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 2789 1 (𝐶𝐷𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  difn0  3897  xpnz  5472  unixp  5585  inf3lem2  8409  infeq5  8417  cantnflem1  8469  iunfictbso  8820  rankcf  9478  hashfun  13084  hashge3el3dif  13122  s1nzOLD  13240  abssubne0  13904  expnprm  15444  grpn0  17277  pmtr3ncomlem2  17717  pgpfaclem2  18304  isdrng2  18580  mpfrcl  19339  ply1frcl  19504  gzrngunit  19631  zringunit  19655  prmirredlem  19660  uvcf1  19950  lindfrn  19979  dfac14lem  21230  flimclslem  21598  lebnumlem3  22570  pmltpclem2  23025  i1fmullem  23267  fta1glem1  23729  fta1blem  23732  dgrcolem1  23833  plydivlem4  23855  plyrem  23864  facth  23865  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  vieta1  23871  aalioulem2  23892  geolim3  23898  logcj  24156  argregt0  24160  argimgt0  24162  argimlt0  24163  logneg2  24165  tanarg  24169  logtayl  24206  cxpsqrt  24249  cxpcn3lem  24288  cxpcn3  24289  dcubic2  24371  dcubic  24373  cubic  24376  asinlem  24395  atandmcj  24436  atancj  24437  atanlogsublem  24442  bndatandm  24456  birthdaylem1  24478  basellem4  24610  basellem5  24611  dchrn0  24775  lgsne0  24860  constr3lem2  26174  nmlno0lem  27032  nmlnop0iALT  28238  cntnevol  29618  signsvtn0  29973  signstfveq0a  29979  signstfveq0  29980  nepss  30854  elima4  30924  heicant  32614  totbndbnd  32758  cdleme3c  34535  cdleme7e  34552  imadisjlnd  37479  compne  37665  stoweidlem39  38932  usgr2trlncl  40966
 Copyright terms: Public domain W3C validator