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

Theorem necon3bii 2994
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 2988 . 2 (𝐴𝐵 ↔ ¬ 𝐶 = 𝐷)
3 df-ne 2942 . 2 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
42, 3bitr4i 278 1 (𝐴𝐵𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1542  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:  necom  2995  neeq1i  3006  neeq2i  3007  neeq12i  3008  rnsnn0  6204  onoviun  8338  onnseq  8339  intrnfi  9407  wdomtr  9566  noinfep  9651  wemapwe  9688  scott0s  9879  cplem1  9880  karden  9886  acndom2  10045  dfac5lem3  10116  fin23lem31  10334  fin23lem40  10342  isf34lem5  10369  isf34lem7  10370  isf34lem6  10371  axrrecex  11154  negne0bi  11529  rpnnen1lem4  12960  rpnnen1lem5  12961  fseqsupcl  13938  limsupgre  15421  isercolllem3  15609  rpnnen2lem12  16164  ruclem11  16179  3dvds  16270  prmreclem6  16850  0ram  16949  0ram2  16950  0ramcl  16952  gsumval2  18601  ghmrn  19099  gexex  19713  gsumval3  19767  subdrgint  20407  iinopn  22386  cnconn  22908  1stcfb  22931  qtopeu  23202  fbasrn  23370  alexsublem  23530  evth  24457  minveclem1  24923  minveclem3b  24927  ovollb2  24988  ovolunlem1a  24995  ovolunlem1  24996  ovoliunlem1  25001  ovoliun2  25005  ioombl1lem4  25060  uniioombllem1  25080  uniioombllem2  25082  uniioombllem6  25087  mbfsup  25163  mbfinf  25164  mbflimsup  25165  itg1climres  25214  itg2monolem1  25250  itg2mono  25253  itg2i1fseq2  25256  sincos4thpi  26005  nosepnelem  27162  axlowdimlem13  28192  eulerpath  29474  siii  30084  minvecolem1  30105  bcsiALT  30410  h1de2bi  30785  h1de2ctlem  30786  nmlnopgt0i  31228  dimval  32632  dimvalfi  32633  rge0scvg  32867  umgracycusgr  34083  cusgracyclt3v  34085  erdszelem5  34124  cvmsss2  34203  elrn3  34670  rankeq1o  35081  fin2so  36413  heicant  36461  scottn0f  36976  psspwb  40994  fnwe2lem2  41726  sqrtcval  42325
  Copyright terms: Public domain W3C validator