Theorem necon3bii 3070

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necom  3071  neeq1i  3082  neeq2i  3083  neeq12i  3084  rnsnn0  6067  onoviun  7982  onnseq  7983  intrnfi  8882  wdomtr  9041  noinfep  9125  wemapwe  9162  scott0s  9319  cplem1  9320  karden  9326  acndom2  9482  dfac5lem3  9553  fin23lem31  9767  fin23lem40  9775  isf34lem5  9802  isf34lem7  9803  isf34lem6  9804  axrrecex  10587  negne0bi  10961  rpnnen1lem4  12382  rpnnen1lem5  12383  fseqsupcl  13348  limsupgre  14840  isercolllem3  15025  rpnnen2lem12  15580  ruclem11  15595  3dvds  15682  prmreclem6  16259  0ram  16358  0ram2  16359  0ramcl  16361  gsumval2  17898  ghmrn  18373  gexex  18975  gsumval3  19029  subdrgint  19584  iinopn  21512  cnconn  22032  1stcfb  22055  qtopeu  22326  fbasrn  22494  alexsublem  22654  evth  23565  minveclem1  24029  minveclem3b  24033  ovollb2  24092  ovolunlem1a  24099  ovolunlem1  24100  ovoliunlem1  24105  ovoliun2  24109  ioombl1lem4  24164  uniioombllem1  24184  uniioombllem2  24186  uniioombllem6  24191  mbfsup  24267  mbfinf  24268  mbflimsup  24269  itg1climres  24317  itg2monolem1  24353  itg2mono  24356  itg2i1fseq2  24359  sincos4thpi  25101  axlowdimlem13  26742  eulerpath  28022  siii  28632  minvecolem1  28653  bcsiALT  28958  h1de2bi  29333  h1de2ctlem  29334  nmlnopgt0i  29776  dimval  31003  dimvalfi  31004  rge0scvg  31194  umgracycusgr  32403  cusgracyclt3v  32405  erdszelem5  32444  cvmsss2  32523  elrn3  33000  nosepnelem  33186  rankeq1o  33634  fin2so  34881  heicant  34929  scottn0f  35450  psspwb  39121  fnwe2lem2  39658