Theorem necon3bii 2987

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

Syntax hints:  ¬ wn 3   ↔ wb 207   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necom  2988  neeq1i  2999  neeq2i  3000  neeq12i  3001  rnsnn0  6166  onoviun  8280  onnseq  8281  intrnfi  9326  wdomtr  9487  noinfep  9579  wemapwe  9616  scott0s  9810  cplem1  9811  karden  9817  acndom2  9974  dfac5lem3  10045  fin23lem31  10263  fin23lem40  10271  isf34lem5  10298  isf34lem7  10299  isf34lem6  10300  axrrecex  11084  negne0bi  11465  rpnnen1lem4  12928  rpnnen1lem5  12929  fseqsupcl  13937  limsupgre  15441  isercolllem3  15627  rpnnen2lem12  16190  ruclem11  16205  3dvds  16298  prmreclem6  16890  0ram  16989  0ram2  16990  0ramcl  16992  gsumval2  18652  ghmrn  19202  gexex  19826  gsumval3  19880  subdrgint  20782  iinopn  22892  cnconn  23412  1stcfb  23435  qtopeu  23706  fbasrn  23874  alexsublem  24034  evth  24951  minveclem1  25416  minveclem3b  25420  ovollb2  25481  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliun2  25498  ioombl1lem4  25553  uniioombllem1  25573  uniioombllem2  25575  uniioombllem6  25580  mbfsup  25656  mbfinf  25657  mbflimsup  25658  itg1climres  25706  itg2monolem1  25742  itg2mono  25745  itg2i1fseq2  25748  sincos4thpi  26502  nosepnelem  27668  axlowdimlem13  29048  eulerpath  30336  siii  30949  minvecolem1  30970  bcsiALT  31275  h1de2bi  31650  h1de2ctlem  31651  nmlnopgt0i  32093  wrdpmtrlast  33181  dimval  33792  dimvalfi  33793  rge0scvg  34140  umgracycusgr  35389  cusgracyclt3v  35391  erdszelem5  35430  cvmsss2  35509  elrn3  35997  rankeq1o  36406  ttc0elw  36762  ttc0el  36770  regsfromunir1  36775  fin2so  37981  heicant  38029  scottn0f  38544  psspwb  42722  fnwe2lem2  43503  sqrtcval  44092