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

Theorem necon3bii 2984
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 2978 . 2 (𝐴𝐵 ↔ ¬ 𝐶 = 𝐷)
3 df-ne 2933 . 2 (𝐶𝐷 ↔ ¬ 𝐶 = 𝐷)
42, 3bitr4i 267 1 (𝐴𝐵𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1632  wne 2932
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 197  df-ne 2933
This theorem is referenced by:  necom  2985  neeq1i  2996  neeq2i  2997  neeq12i  2998  rnsnn0  5759  onoviun  7609  onnseq  7610  intrnfi  8487  wdomtr  8645  noinfep  8730  wemapwe  8767  scott0s  8924  cplem1  8925  karden  8931  acndom2  9067  dfac5lem3  9138  fin23lem31  9357  fin23lem40  9365  isf34lem5  9392  isf34lem7  9393  isf34lem6  9394  axrrecex  10176  negne0bi  10546  rpnnen1lem4  12010  rpnnen1lem5  12011  rpnnen1lem4OLD  12016  rpnnen1lem5OLD  12017  fseqsupcl  12970  limsupgre  14411  isercolllem3  14596  rpnnen2lem12  15153  ruclem11  15168  3dvds  15254  3dvdsOLD  15255  prmreclem6  15827  0ram  15926  0ram2  15927  0ramcl  15929  gsumval2  17481  ghmrn  17874  gexex  18456  gsumval3  18508  iinopn  20909  cnconn  21427  1stcfb  21450  qtopeu  21721  fbasrn  21889  alexsublem  22049  evth  22959  minveclem1  23395  minveclem3b  23399  ovollb2  23457  ovolunlem1a  23464  ovolunlem1  23465  ovoliunlem1  23470  ovoliun2  23474  ioombl1lem4  23529  uniioombllem1  23549  uniioombllem2  23551  uniioombllem6  23556  mbfsup  23630  mbfinf  23631  mbflimsup  23632  itg1climres  23680  itg2monolem1  23716  itg2mono  23719  itg2i1fseq2  23722  sincos4thpi  24464  axlowdimlem13  26033  eulerpath  27393  siii  28017  minvecolem1  28039  bcsiALT  28345  h1de2bi  28722  h1de2ctlem  28723  nmlnopgt0i  29165  rge0scvg  30304  erdszelem5  31484  cvmsss2  31563  elrn3  31959  nosepnelem  32136  rankeq1o  32584  fin2so  33709  heicant  33757  scottn0f  34291  fnwe2lem2  38123  wnefimgd  38962
  Copyright terms: Public domain W3C validator