Theorem necon3bii 2983

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

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

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 2931

This theorem is referenced by:  necom  2984  neeq1i  2995  neeq2i  2996  neeq12i  2997  rnsnn0  6207  onoviun  8362  onnseq  8363  intrnfi  9439  wdomtr  9598  noinfep  9683  wemapwe  9720  scott0s  9911  cplem1  9912  karden  9918  acndom2  10077  dfac5lem3  10148  fin23lem31  10366  fin23lem40  10374  isf34lem5  10401  isf34lem7  10402  isf34lem6  10403  axrrecex  11186  negne0bi  11563  rpnnen1lem4  12994  rpnnen1lem5  12995  fseqsupcl  13974  limsupgre  15457  isercolllem3  15645  rpnnen2lem12  16201  ruclem11  16216  3dvds  16307  prmreclem6  16889  0ram  16988  0ram2  16989  0ramcl  16991  gsumval2  18645  ghmrn  19187  gexex  19812  gsumval3  19866  subdrgint  20695  iinopn  22822  cnconn  23344  1stcfb  23367  qtopeu  23638  fbasrn  23806  alexsublem  23966  evth  24903  minveclem1  25370  minveclem3b  25374  ovollb2  25436  ovolunlem1a  25443  ovolunlem1  25444  ovoliunlem1  25449  ovoliun2  25453  ioombl1lem4  25508  uniioombllem1  25528  uniioombllem2  25530  uniioombllem6  25535  mbfsup  25611  mbfinf  25612  mbflimsup  25613  itg1climres  25662  itg2monolem1  25698  itg2mono  25701  itg2i1fseq2  25704  sincos4thpi  26466  nosepnelem  27630  axlowdimlem13  28809  eulerpath  30095  siii  30707  minvecolem1  30728  bcsiALT  31033  h1de2bi  31408  h1de2ctlem  31409  nmlnopgt0i  31851  dimval  33355  dimvalfi  33356  rge0scvg  33607  umgracycusgr  34821  cusgracyclt3v  34823  erdszelem5  34862  cvmsss2  34941  elrn3  35413  rankeq1o  35824  fin2so  37137  heicant  37185  scottn0f  37700  psspwb  41772  fnwe2lem2  42540  sqrtcval  43136