Theorem necon3bii 2977

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 2971	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐶 = 𝐷)
3		df-ne 2926	. 2 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
4	2, 3	bitr4i 278	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necom  2978  neeq1i  2989  neeq2i  2990  neeq12i  2991  rnsnn0  6181  onoviun  8312  onnseq  8313  intrnfi  9367  wdomtr  9528  noinfep  9613  wemapwe  9650  scott0s  9841  cplem1  9842  karden  9848  acndom2  10007  dfac5lem3  10078  fin23lem31  10296  fin23lem40  10304  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  axrrecex  11116  negne0bi  11495  rpnnen1lem4  12939  rpnnen1lem5  12940  fseqsupcl  13942  limsupgre  15447  isercolllem3  15633  rpnnen2lem12  16193  ruclem11  16208  3dvds  16301  prmreclem6  16892  0ram  16991  0ram2  16992  0ramcl  16994  gsumval2  18613  ghmrn  19161  gexex  19783  gsumval3  19837  subdrgint  20712  iinopn  22789  cnconn  23309  1stcfb  23332  qtopeu  23603  fbasrn  23771  alexsublem  23931  evth  24858  minveclem1  25324  minveclem3b  25328  ovollb2  25390  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun2  25407  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem2  25484  uniioombllem6  25489  mbfsup  25565  mbfinf  25566  mbflimsup  25567  itg1climres  25615  itg2monolem1  25651  itg2mono  25654  itg2i1fseq2  25657  sincos4thpi  26422  nosepnelem  27591  axlowdimlem13  28881  eulerpath  30170  siii  30782  minvecolem1  30803  bcsiALT  31108  h1de2bi  31483  h1de2ctlem  31484  nmlnopgt0i  31926  wrdpmtrlast  33050  dimval  33596  dimvalfi  33597  rge0scvg  33939  umgracycusgr  35141  cusgracyclt3v  35143  erdszelem5  35182  cvmsss2  35261  elrn3  35749  rankeq1o  36159  fin2so  37601  heicant  37649  scottn0f  38164  psspwb  42216  fnwe2lem2  43040  sqrtcval  43630