Theorem necon3bii 2999

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necom  3000  neeq1i  3011  neeq2i  3012  neeq12i  3013  rnsnn0  6239  onoviun  8399  onnseq  8400  intrnfi  9485  wdomtr  9644  noinfep  9729  wemapwe  9766  scott0s  9957  cplem1  9958  karden  9964  acndom2  10123  dfac5lem3  10194  fin23lem31  10412  fin23lem40  10420  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  axrrecex  11232  negne0bi  11609  rpnnen1lem4  13045  rpnnen1lem5  13046  fseqsupcl  14028  limsupgre  15527  isercolllem3  15715  rpnnen2lem12  16273  ruclem11  16288  3dvds  16379  prmreclem6  16968  0ram  17067  0ram2  17068  0ramcl  17070  gsumval2  18724  ghmrn  19269  gexex  19895  gsumval3  19949  subdrgint  20826  iinopn  22929  cnconn  23451  1stcfb  23474  qtopeu  23745  fbasrn  23913  alexsublem  24073  evth  25010  minveclem1  25477  minveclem3b  25481  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem6  25642  mbfsup  25718  mbfinf  25719  mbflimsup  25720  itg1climres  25769  itg2monolem1  25805  itg2mono  25808  itg2i1fseq2  25811  sincos4thpi  26573  nosepnelem  27742  axlowdimlem13  28987  eulerpath  30273  siii  30885  minvecolem1  30906  bcsiALT  31211  h1de2bi  31586  h1de2ctlem  31587  nmlnopgt0i  32029  wrdpmtrlast  33086  dimval  33613  dimvalfi  33614  rge0scvg  33895  umgracycusgr  35122  cusgracyclt3v  35124  erdszelem5  35163  cvmsss2  35242  elrn3  35724  rankeq1o  36135  fin2so  37567  heicant  37615  scottn0f  38130  psspwb  42221  fnwe2lem2  43008  sqrtcval  43603