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

Theorem necon3i 2974
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 2966 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 2948 1 (𝐶𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wne 2941
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 2942
This theorem is referenced by:  difn0  4322  xpnz  6109  unixp  6232  inf3lem2  9561  infeq5  9569  cantnflem1  9621  iunfictbso  10046  rankcf  10709  hashfun  14329  hashge3el3dif  14377  abssubne0  15193  expnprm  16766  grpn0  18774  pmtr3ncomlem2  19247  pgpfaclem2  19852  isdrng2  20183  gzrngunit  20848  zringunit  20872  prmirredlem  20878  uvcf1  21183  lindfrn  21212  mpfrcl  21479  ply1frcl  21668  dfac14lem  22952  flimclslem  23319  lebnumlem3  24310  pmltpclem2  24797  i1fmullem  25042  fta1glem1  25514  fta1blem  25517  dgrcolem1  25618  plydivlem4  25640  plyrem  25649  facth  25650  fta1lem  25651  vieta1lem1  25654  vieta1lem2  25655  vieta1  25656  aalioulem2  25677  geolim3  25683  logcj  25945  argregt0  25949  argimgt0  25951  argimlt0  25952  logneg2  25954  tanarg  25958  logtayl  25999  cxpsqrt  26042  cxpcn3lem  26084  cxpcn3  26085  dcubic2  26178  dcubic  26180  cubic  26183  asinlem  26202  atandmcj  26243  atancj  26244  atanlogsublem  26249  bndatandm  26263  birthdaylem1  26285  basellem4  26417  dchrn0  26582  lgsne0  26667  usgr2trlncl  28594  nmlno0lem  29621  nmlnop0iALT  30823  eldmne0  31428  preimane  31472  prmidl0  32102  cntnevol  32696  signsvtn0  33051  signstfveq0a  33057  signstfveq0  33058  nepss  34158  elima4  34220  heicant  36080  totbndbnd  36215  cdleme3c  38660  cdleme7e  38677  uvcn0  40691  sn-1ne2  40719  sn-0ne2  40813  imadisjlnd  42375  compne  42663  stoweidlem39  44212  rrx2vlinest  46759  rrx2linesl  46761  elfvne0  46847
  Copyright terms: Public domain W3C validator