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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1533   ≠ wne 2934

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 206  df-ne 2935

This theorem is referenced by:  necom  2988  neeq1i  2999  neeq2i  3000  neeq12i  3001  rnsnn0  6201  onoviun  8344  onnseq  8345  intrnfi  9413  wdomtr  9572  noinfep  9657  wemapwe  9694  scott0s  9885  cplem1  9886  karden  9892  acndom2  10051  dfac5lem3  10122  fin23lem31  10340  fin23lem40  10348  isf34lem5  10375  isf34lem7  10376  isf34lem6  10377  axrrecex  11160  negne0bi  11537  rpnnen1lem4  12968  rpnnen1lem5  12969  fseqsupcl  13948  limsupgre  15431  isercolllem3  15619  rpnnen2lem12  16175  ruclem11  16190  3dvds  16281  prmreclem6  16863  0ram  16962  0ram2  16963  0ramcl  16965  gsumval2  18619  ghmrn  19154  gexex  19773  gsumval3  19827  subdrgint  20654  iinopn  22759  cnconn  23281  1stcfb  23304  qtopeu  23575  fbasrn  23743  alexsublem  23903  evth  24840  minveclem1  25307  minveclem3b  25311  ovollb2  25373  ovolunlem1a  25380  ovolunlem1  25381  ovoliunlem1  25386  ovoliun2  25390  ioombl1lem4  25445  uniioombllem1  25465  uniioombllem2  25467  uniioombllem6  25472  mbfsup  25548  mbfinf  25549  mbflimsup  25550  itg1climres  25599  itg2monolem1  25635  itg2mono  25638  itg2i1fseq2  25641  sincos4thpi  26403  nosepnelem  27567  axlowdimlem13  28720  eulerpath  30003  siii  30615  minvecolem1  30636  bcsiALT  30941  h1de2bi  31316  h1de2ctlem  31317  nmlnopgt0i  31759  dimval  33203  dimvalfi  33204  rge0scvg  33459  umgracycusgr  34673  cusgracyclt3v  34675  erdszelem5  34714  cvmsss2  34793  elrn3  35265  rankeq1o  35676  fin2so  36988  heicant  37036  scottn0f  37551  psspwb  41607  fnwe2lem2  42371  sqrtcval  42968