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  6161  onoviun  8273  onnseq  8274  intrnfi  9325  wdomtr  9486  noinfep  9575  wemapwe  9612  scott0s  9803  cplem1  9804  karden  9810  acndom2  9967  dfac5lem3  10038  fin23lem31  10256  fin23lem40  10264  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axrrecex  11076  negne0bi  11455  rpnnen1lem4  12899  rpnnen1lem5  12900  fseqsupcl  13902  limsupgre  15406  isercolllem3  15592  rpnnen2lem12  16152  ruclem11  16167  3dvds  16260  prmreclem6  16851  0ram  16950  0ram2  16951  0ramcl  16953  gsumval2  18578  ghmrn  19126  gexex  19750  gsumval3  19804  subdrgint  20706  iinopn  22805  cnconn  23325  1stcfb  23348  qtopeu  23619  fbasrn  23787  alexsublem  23947  evth  24874  minveclem1  25340  minveclem3b  25344  ovollb2  25406  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliun2  25423  ioombl1lem4  25478  uniioombllem1  25498  uniioombllem2  25500  uniioombllem6  25505  mbfsup  25581  mbfinf  25582  mbflimsup  25583  itg1climres  25631  itg2monolem1  25667  itg2mono  25670  itg2i1fseq2  25673  sincos4thpi  26438  nosepnelem  27607  axlowdimlem13  28917  eulerpath  30203  siii  30815  minvecolem1  30836  bcsiALT  31141  h1de2bi  31516  h1de2ctlem  31517  nmlnopgt0i  31959  wrdpmtrlast  33048  dimval  33575  dimvalfi  33576  rge0scvg  33918  umgracycusgr  35129  cusgracyclt3v  35131  erdszelem5  35170  cvmsss2  35249  elrn3  35737  rankeq1o  36147  fin2so  37589  heicant  37637  scottn0f  38152  psspwb  42204  fnwe2lem2  43027  sqrtcval  43617