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

Theorem necon3bii 3065
Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
Hypothesis
Ref Expression
necon3bii.1 (𝐴 = 𝐵𝐶 = 𝐷)
Assertion
Ref Expression
necon3bii (𝐴𝐵𝐶𝐷)

Proof of Theorem necon3bii
StepHypRef Expression
1 necon3bii.1 . . 3 (𝐴 = 𝐵𝐶 = 𝐷)
21necon3abii 3059 . 2 (𝐴𝐵 ↔ ¬ 𝐶 = 𝐷)
3 df-ne 3014 . 2 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
42, 3bitr4i 281 1 (𝐴𝐵𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209   = wceq 1538  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 210  df-ne 3014
This theorem is referenced by:  necom  3066  neeq1i  3077  neeq2i  3078  neeq12i  3079  rnsnn0  6048  onoviun  7965  onnseq  7966  intrnfi  8866  wdomtr  9025  noinfep  9109  wemapwe  9146  scott0s  9303  cplem1  9304  karden  9310  acndom2  9467  dfac5lem3  9538  fin23lem31  9752  fin23lem40  9760  isf34lem5  9787  isf34lem7  9788  isf34lem6  9789  axrrecex  10572  negne0bi  10946  rpnnen1lem4  12367  rpnnen1lem5  12368  fseqsupcl  13340  limsupgre  14829  isercolllem3  15014  rpnnen2lem12  15569  ruclem11  15584  3dvds  15671  prmreclem6  16246  0ram  16345  0ram2  16346  0ramcl  16348  gsumval2  17887  ghmrn  18362  gexex  18964  gsumval3  19018  subdrgint  19570  iinopn  21498  cnconn  22018  1stcfb  22041  qtopeu  22312  fbasrn  22480  alexsublem  22640  evth  23555  minveclem1  24019  minveclem3b  24023  ovollb2  24084  ovolunlem1a  24091  ovolunlem1  24092  ovoliunlem1  24097  ovoliun2  24101  ioombl1lem4  24156  uniioombllem1  24176  uniioombllem2  24178  uniioombllem6  24183  mbfsup  24259  mbfinf  24260  mbflimsup  24261  itg1climres  24309  itg2monolem1  24345  itg2mono  24348  itg2i1fseq2  24351  sincos4thpi  25097  axlowdimlem13  26739  eulerpath  28017  siii  28627  minvecolem1  28648  bcsiALT  28953  h1de2bi  29328  h1de2ctlem  29329  nmlnopgt0i  29771  dimval  31024  dimvalfi  31025  rge0scvg  31212  umgracycusgr  32421  cusgracyclt3v  32423  erdszelem5  32462  cvmsss2  32541  elrn3  33018  nosepnelem  33204  rankeq1o  33652  fin2so  34949  heicant  34997  scottn0f  35513  psspwb  39280  fnwe2lem2  39842  sqrtcval  40188
  Copyright terms: Public domain W3C validator