Theorem necon3bii 2875

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

Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necom  2876  neeq1i  2887  neeq2i  2888  neeq12i  2889  rnsnn0  5636  onoviun  7485  onnseq  7486  intrnfi  8363  wdomtr  8521  noinfep  8595  wemapwe  8632  scott0s  8789  cplem1  8790  karden  8796  acndom2  8915  dfac5lem3  8986  fin23lem31  9203  fin23lem40  9211  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  axrrecex  10022  negne0bi  10392  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  fseqsupcl  12816  limsupgre  14256  isercolllem3  14441  rpnnen2lem12  14998  ruclem11  15013  3dvds  15099  3dvdsOLD  15100  prmreclem6  15672  0ram  15771  0ram2  15772  0ramcl  15774  gsumval2  17327  ghmrn  17720  gexex  18302  gsumval3  18354  iinopn  20755  cnconn  21273  1stcfb  21296  qtopeu  21567  fbasrn  21735  alexsublem  21895  evth  22805  minveclem1  23241  minveclem3b  23245  ovollb2  23303  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliun2  23320  ioombl1lem4  23375  uniioombllem1  23395  uniioombllem2  23397  uniioombllem6  23402  mbfsup  23476  mbfinf  23477  mbflimsup  23478  itg1climres  23526  itg2monolem1  23562  itg2mono  23565  itg2i1fseq2  23568  sincos4thpi  24310  axlowdimlem13  25879  eulerpath  27219  siii  27836  minvecolem1  27858  bcsiALT  28164  h1de2bi  28541  h1de2ctlem  28542  nmlnopgt0i  28984  rge0scvg  30123  erdszelem5  31303  cvmsss2  31382  elrn3  31778  nosepnelem  31955  rankeq1o  32403  fin2so  33526  heicant  33574  scottn0f  34108  fnwe2lem2  37938  wnefimgd  38777