Theorem necon3bii 2996

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  necom  2997  neeq1i  3008  neeq2i  3009  neeq12i  3010  rnsnn0  6111  onoviun  8174  onnseq  8175  intrnfi  9175  wdomtr  9334  noinfep  9418  wemapwe  9455  scott0s  9646  cplem1  9647  karden  9653  acndom2  9810  dfac5lem3  9881  fin23lem31  10099  fin23lem40  10107  isf34lem5  10134  isf34lem7  10135  isf34lem6  10136  axrrecex  10919  negne0bi  11294  rpnnen1lem4  12720  rpnnen1lem5  12721  fseqsupcl  13697  limsupgre  15190  isercolllem3  15378  rpnnen2lem12  15934  ruclem11  15949  3dvds  16040  prmreclem6  16622  0ram  16721  0ram2  16722  0ramcl  16724  gsumval2  18370  ghmrn  18847  gexex  19454  gsumval3  19508  subdrgint  20071  iinopn  22051  cnconn  22573  1stcfb  22596  qtopeu  22867  fbasrn  23035  alexsublem  23195  evth  24122  minveclem1  24588  minveclem3b  24592  ovollb2  24653  ovolunlem1a  24660  ovolunlem1  24661  ovoliunlem1  24666  ovoliun2  24670  ioombl1lem4  24725  uniioombllem1  24745  uniioombllem2  24747  uniioombllem6  24752  mbfsup  24828  mbfinf  24829  mbflimsup  24830  itg1climres  24879  itg2monolem1  24915  itg2mono  24918  itg2i1fseq2  24921  sincos4thpi  25670  axlowdimlem13  27322  eulerpath  28605  siii  29215  minvecolem1  29236  bcsiALT  29541  h1de2bi  29916  h1de2ctlem  29917  nmlnopgt0i  30359  dimval  31686  dimvalfi  31687  rge0scvg  31899  umgracycusgr  33116  cusgracyclt3v  33118  erdszelem5  33157  cvmsss2  33236  elrn3  33729  nosepnelem  33882  rankeq1o  34473  fin2so  35764  heicant  35812  scottn0f  36328  psspwb  40203  fnwe2lem2  40876  sqrtcval  41249