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

Theorem necon3bii 2993
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 2987 . 2 (𝐴𝐵 ↔ ¬ 𝐶 = 𝐷)
3 df-ne 2941 . 2 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
42, 3bitr4i 278 1 (𝐴𝐵𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206   = wceq 1540  wne 2940
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 207  df-ne 2941
This theorem is referenced by:  necom  2994  neeq1i  3005  neeq2i  3006  neeq12i  3007  rnsnn0  6228  onoviun  8383  onnseq  8384  intrnfi  9456  wdomtr  9615  noinfep  9700  wemapwe  9737  scott0s  9928  cplem1  9929  karden  9935  acndom2  10094  dfac5lem3  10165  fin23lem31  10383  fin23lem40  10391  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  axrrecex  11203  negne0bi  11582  rpnnen1lem4  13022  rpnnen1lem5  13023  fseqsupcl  14018  limsupgre  15517  isercolllem3  15703  rpnnen2lem12  16261  ruclem11  16276  3dvds  16368  prmreclem6  16959  0ram  17058  0ram2  17059  0ramcl  17061  gsumval2  18699  ghmrn  19247  gexex  19871  gsumval3  19925  subdrgint  20804  iinopn  22908  cnconn  23430  1stcfb  23453  qtopeu  23724  fbasrn  23892  alexsublem  24052  evth  24991  minveclem1  25458  minveclem3b  25462  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun2  25541  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  mbfsup  25699  mbfinf  25700  mbflimsup  25701  itg1climres  25749  itg2monolem1  25785  itg2mono  25788  itg2i1fseq2  25791  sincos4thpi  26555  nosepnelem  27724  axlowdimlem13  28969  eulerpath  30260  siii  30872  minvecolem1  30893  bcsiALT  31198  h1de2bi  31573  h1de2ctlem  31574  nmlnopgt0i  32016  wrdpmtrlast  33113  dimval  33651  dimvalfi  33652  rge0scvg  33948  umgracycusgr  35159  cusgracyclt3v  35161  erdszelem5  35200  cvmsss2  35279  elrn3  35762  rankeq1o  36172  fin2so  37614  heicant  37662  scottn0f  38177  psspwb  42267  fnwe2lem2  43063  sqrtcval  43654
  Copyright terms: Public domain W3C validator