Theorem necon3bii 3008

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necom  3009  neeq1i  3020  neeq2i  3021  neeq12i  3022  rnsnn0  6202  onoviun  8335  onnseq  8336  intrnfi  9392  wdomtr  9553  noinfep  9645  wemapwe  9682  scott0bs  9925  scott0bsOLD  9926  cplem1  9931  cplem1OLD  9932  karden  9940  kardenOLD  9941  acndom2  10114  dfac5lem3  10185  fin23lem31  10402  fin23lem40  10410  isf34lem5  10437  isf34lem7  10438  isf34lem6  10439  axrrecex  11229  negne0bi  11612  rpnnen1lem4  13089  rpnnen1lem5  13090  fseqsupcl  14100  limsupgre  15628  isercolllem3  15814  rpnnen2lem12  16373  ruclem11  16388  3dvds  16481  prmreclem6  17079  0ram  17178  0ram2  17179  0ramcl  17181  gsumval2  18855  ghmrn  19423  gexex  20047  gsumval3  20101  subdrgint  21040  iinopn  23200  cnconn  23720  1stcfb  23743  qtopeu  24015  fbasrn  24183  alexsublem  24343  evth  25260  minveclem1  25725  minveclem3b  25729  ovollb2  25790  ovolunlem1a  25797  ovolunlem1  25798  ovoliunlem1  25803  ovoliun2  25807  ioombl1lem4  25862  uniioombllem1  25882  uniioombllem2  25884  uniioombllem6  25889  mbfsup  25965  mbfinf  25966  mbflimsup  25967  itg1climres  26015  itg2monolem1  26051  itg2mono  26054  itg2i1fseq2  26057  sincos4thpi  26824  nosepnelem  28018  axlowdimlem13  29514  eulerpath  30824  siii  31437  minvecolem1  31458  bcsiALT  31763  h1de2bi  32138  h1de2ctlem  32139  nmlnopgt0i  32581  wrdpmtrlast  33636  dimval  34215  dimvalfi  34216  rge0scvg  34563  rankscott  35730  kardeq0  35797  umgracycusgr  35888  cusgracyclt3v  35890  erdszelem5  35929  cvmsss2  36008  elrn3  36496  rankeq1o  36902  ttc0elw  37285  ttc0el  37293  regsfromunir1  37298  fin2so  38498  heicant  38541  scottn0f  39070  psspwb  43250  fnwe2lem2  44011  sqrtcval  44600