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

Step	Hyp	Ref	Expression
1		necon3bii.1	. . 3 ⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)
2	1	necon3abii 2978	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷)
3		df-ne 2933	. 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
4	2, 3	bitr4i 278	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ 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 207  df-ne 2933

This theorem is referenced by:  necom  2985  neeq1i  2996  neeq2i  2997  neeq12i  2998  rnsnn0  6197  onoviun  8357  onnseq  8358  intrnfi  9428  wdomtr  9589  noinfep  9674  wemapwe  9711  scott0s  9902  cplem1  9903  karden  9909  acndom2  10068  dfac5lem3  10139  fin23lem31  10357  fin23lem40  10365  isf34lem5  10392  isf34lem7  10393  isf34lem6  10394  axrrecex  11177  negne0bi  11556  rpnnen1lem4  12996  rpnnen1lem5  12997  fseqsupcl  13995  limsupgre  15497  isercolllem3  15683  rpnnen2lem12  16243  ruclem11  16258  3dvds  16350  prmreclem6  16941  0ram  17040  0ram2  17041  0ramcl  17043  gsumval2  18664  ghmrn  19212  gexex  19834  gsumval3  19888  subdrgint  20763  iinopn  22840  cnconn  23360  1stcfb  23383  qtopeu  23654  fbasrn  23822  alexsublem  23982  evth  24909  minveclem1  25376  minveclem3b  25380  ovollb2  25442  ovolunlem1a  25449  ovolunlem1  25450  ovoliunlem1  25455  ovoliun2  25459  ioombl1lem4  25514  uniioombllem1  25534  uniioombllem2  25536  uniioombllem6  25541  mbfsup  25617  mbfinf  25618  mbflimsup  25619  itg1climres  25667  itg2monolem1  25703  itg2mono  25706  itg2i1fseq2  25709  sincos4thpi  26474  nosepnelem  27643  axlowdimlem13  28933  eulerpath  30222  siii  30834  minvecolem1  30855  bcsiALT  31160  h1de2bi  31535  h1de2ctlem  31536  nmlnopgt0i  31978  wrdpmtrlast  33104  dimval  33640  dimvalfi  33641  rge0scvg  33980  umgracycusgr  35176  cusgracyclt3v  35178  erdszelem5  35217  cvmsss2  35296  elrn3  35779  rankeq1o  36189  fin2so  37631  heicant  37679  scottn0f  38194  psspwb  42279  fnwe2lem2  43075  sqrtcval  43665