Theorem necon3bii 2978

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

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

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 2927

This theorem is referenced by:  necom  2979  neeq1i  2990  neeq2i  2991  neeq12i  2992  rnsnn0  6184  onoviun  8315  onnseq  8316  intrnfi  9374  wdomtr  9535  noinfep  9620  wemapwe  9657  scott0s  9848  cplem1  9849  karden  9855  acndom2  10014  dfac5lem3  10085  fin23lem31  10303  fin23lem40  10311  isf34lem5  10338  isf34lem7  10339  isf34lem6  10340  axrrecex  11123  negne0bi  11502  rpnnen1lem4  12946  rpnnen1lem5  12947  fseqsupcl  13949  limsupgre  15454  isercolllem3  15640  rpnnen2lem12  16200  ruclem11  16215  3dvds  16308  prmreclem6  16899  0ram  16998  0ram2  16999  0ramcl  17001  gsumval2  18620  ghmrn  19168  gexex  19790  gsumval3  19844  subdrgint  20719  iinopn  22796  cnconn  23316  1stcfb  23339  qtopeu  23610  fbasrn  23778  alexsublem  23938  evth  24865  minveclem1  25331  minveclem3b  25335  ovollb2  25397  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun2  25414  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem2  25491  uniioombllem6  25496  mbfsup  25572  mbfinf  25573  mbflimsup  25574  itg1climres  25622  itg2monolem1  25658  itg2mono  25661  itg2i1fseq2  25664  sincos4thpi  26429  nosepnelem  27598  axlowdimlem13  28888  eulerpath  30177  siii  30789  minvecolem1  30810  bcsiALT  31115  h1de2bi  31490  h1de2ctlem  31491  nmlnopgt0i  31933  wrdpmtrlast  33057  dimval  33603  dimvalfi  33604  rge0scvg  33946  umgracycusgr  35148  cusgracyclt3v  35150  erdszelem5  35189  cvmsss2  35268  elrn3  35756  rankeq1o  36166  fin2so  37608  heicant  37656  scottn0f  38171  psspwb  42223  fnwe2lem2  43047  sqrtcval  43637