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

Theorem necon3bii 2834
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 2828 . 2 (𝐴𝐵 ↔ ¬ 𝐶 = 𝐷)
3 df-ne 2782 . 2 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
42, 3bitr4i 266 1 (𝐴𝐵𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195   = 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:  necom  2835  neeq1i  2846  neeq2i  2847  neeq12i  2848  rnsnn0  5519  onoviun  7327  onnseq  7328  intrnfi  8205  wdomtr  8363  noinfep  8440  wemapwe  8477  scott0s  8634  cplem1  8635  karden  8641  acndom2  8760  dfac5lem3  8831  fin23lem31  9048  fin23lem40  9056  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  axrrecex  9863  negne0bi  10233  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  fseqsupcl  12638  limsupgre  14060  isercolllem3  14245  rpnnen2lem12  14793  ruclem11  14808  3dvds  14890  3dvdsOLD  14891  prmreclem6  15463  0ram  15562  0ram2  15563  0ramcl  15565  gsumval2  17103  ghmrn  17496  gexex  18079  gsumval3  18131  iinopn  20532  cnconn  21035  1stcfb  21058  qtopeu  21329  fbasrn  21498  alexsublem  21658  evth  22566  minveclem1  23003  minveclem3b  23007  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliun2  23081  ioombl1lem4  23136  uniioombllem1  23155  uniioombllem2  23157  uniioombllem6  23162  mbfsup  23237  mbfinf  23238  mbflimsup  23239  itg1climres  23287  itg2monolem1  23323  itg2mono  23326  itg2i1fseq2  23329  sincos4thpi  24069  axlowdimlem13  25634  eupath  26508  siii  27092  minvecolem1  27114  bcsiALT  27420  h1de2bi  27797  h1de2ctlem  27798  nmlnopgt0i  28240  rge0scvg  29323  erdszelem5  30431  cvmsss2  30510  elrn3  30906  rankeq1o  31448  fin2so  32566  heicant  32614  scottn0f  33148  fnwe2lem2  36639  wnefimgd  37480  eulerpath  41409
  Copyright terms: Public domain W3C validator