Theorem necon3bii 3039

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necom  3040  neeq1i  3051  neeq2i  3052  neeq12i  3053  rnsnn0  6032  onoviun  7963  onnseq  7964  intrnfi  8864  wdomtr  9023  noinfep  9107  wemapwe  9144  scott0s  9301  cplem1  9302  karden  9308  acndom2  9465  dfac5lem3  9536  fin23lem31  9754  fin23lem40  9762  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  axrrecex  10574  negne0bi  10948  rpnnen1lem4  12367  rpnnen1lem5  12368  fseqsupcl  13340  limsupgre  14830  isercolllem3  15015  rpnnen2lem12  15570  ruclem11  15585  3dvds  15672  prmreclem6  16247  0ram  16346  0ram2  16347  0ramcl  16349  gsumval2  17888  ghmrn  18363  gexex  18966  gsumval3  19020  subdrgint  19575  iinopn  21507  cnconn  22027  1stcfb  22050  qtopeu  22321  fbasrn  22489  alexsublem  22649  evth  23564  minveclem1  24028  minveclem3b  24032  ovollb2  24093  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliun2  24110  ioombl1lem4  24165  uniioombllem1  24185  uniioombllem2  24187  uniioombllem6  24192  mbfsup  24268  mbfinf  24269  mbflimsup  24270  itg1climres  24318  itg2monolem1  24354  itg2mono  24357  itg2i1fseq2  24360  sincos4thpi  25106  axlowdimlem13  26748  eulerpath  28026  siii  28636  minvecolem1  28657  bcsiALT  28962  h1de2bi  29337  h1de2ctlem  29338  nmlnopgt0i  29780  dimval  31089  dimvalfi  31090  rge0scvg  31302  umgracycusgr  32514  cusgracyclt3v  32516  erdszelem5  32555  cvmsss2  32634  elrn3  33111  nosepnelem  33297  rankeq1o  33745  fin2so  35044  heicant  35092  scottn0f  35608  psspwb  39408  fnwe2lem2  39995  sqrtcval  40341