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

Theorem necon3i 3045
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 3038 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 3020 1 (𝐶𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3013
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 208  df-ne 3014
This theorem is referenced by:  difn0  4321  xpnz  6009  unixp  6126  inf3lem2  9080  infeq5  9088  cantnflem1  9140  iunfictbso  9528  rankcf  10187  hashfun  13786  hashge3el3dif  13832  abssubne0  14664  expnprm  16226  grpn0  18073  pmtr3ncomlem2  18531  pgpfaclem2  19133  isdrng2  19441  mpfrcl  20226  ply1frcl  20409  gzrngunit  20539  zringunit  20563  prmirredlem  20568  uvcf1  20864  lindfrn  20893  dfac14lem  22153  flimclslem  22520  lebnumlem3  23494  pmltpclem2  23977  i1fmullem  24222  fta1glem1  24686  fta1blem  24689  dgrcolem1  24790  plydivlem4  24812  plyrem  24821  facth  24822  fta1lem  24823  vieta1lem1  24826  vieta1lem2  24827  vieta1  24828  aalioulem2  24849  geolim3  24855  logcj  25116  argregt0  25120  argimgt0  25122  argimlt0  25123  logneg2  25125  tanarg  25129  logtayl  25170  cxpsqrt  25213  cxpcn3lem  25255  cxpcn3  25256  dcubic2  25349  dcubic  25351  cubic  25354  asinlem  25373  atandmcj  25414  atancj  25415  atanlogsublem  25420  bndatandm  25434  birthdaylem1  25456  basellem4  25588  dchrn0  25753  lgsne0  25838  usgr2trlncl  27468  nmlno0lem  28497  nmlnop0iALT  29699  eldmne0  30301  preimane  30343  cntnevol  31386  signsvtn0  31739  signstfveq0a  31745  signstfveq0  31746  nepss  32845  elima4  32916  heicant  34808  totbndbnd  34948  cdleme3c  37246  cdleme7e  37263  sn-1ne2  39036  sn-0ne2  39114  imadisjlnd  40389  compne  40650  stoweidlem39  42201  rrx2vlinest  44656  rrx2linesl  44658
  Copyright terms: Public domain W3C validator