Theorem necon3bii 2985

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necom  2986  neeq1i  2997  neeq2i  2998  neeq12i  2999  rnsnn0  6166  onoviun  8276  onnseq  8277  intrnfi  9322  wdomtr  9483  noinfep  9572  wemapwe  9609  scott0s  9803  cplem1  9804  karden  9810  acndom2  9967  dfac5lem3  10038  fin23lem31  10256  fin23lem40  10264  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axrrecex  11077  negne0bi  11458  rpnnen1lem4  12921  rpnnen1lem5  12922  fseqsupcl  13930  limsupgre  15434  isercolllem3  15620  rpnnen2lem12  16183  ruclem11  16198  3dvds  16291  prmreclem6  16883  0ram  16982  0ram2  16983  0ramcl  16985  gsumval2  18645  ghmrn  19195  gexex  19819  gsumval3  19873  subdrgint  20771  iinopn  22877  cnconn  23397  1stcfb  23420  qtopeu  23691  fbasrn  23859  alexsublem  24019  evth  24936  minveclem1  25401  minveclem3b  25405  ovollb2  25466  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovoliun2  25483  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem2  25560  uniioombllem6  25565  mbfsup  25641  mbfinf  25642  mbflimsup  25643  itg1climres  25691  itg2monolem1  25727  itg2mono  25730  itg2i1fseq2  25733  sincos4thpi  26490  nosepnelem  27657  axlowdimlem13  29037  eulerpath  30326  siii  30939  minvecolem1  30960  bcsiALT  31265  h1de2bi  31640  h1de2ctlem  31641  nmlnopgt0i  32083  wrdpmtrlast  33169  dimval  33760  dimvalfi  33761  rge0scvg  34109  umgracycusgr  35352  cusgracyclt3v  35354  erdszelem5  35393  cvmsss2  35472  elrn3  35960  rankeq1o  36369  ttc0elw  36725  ttc0el  36733  regsfromunir1  36738  fin2so  37942  heicant  37990  scottn0f  38505  psspwb  42683  fnwe2lem2  43497  sqrtcval  44086