Theorem necon3bii 2994

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necom  2995  neeq1i  3006  neeq2i  3007  neeq12i  3008  rnsnn0  6204  onoviun  8338  onnseq  8339  intrnfi  9407  wdomtr  9566  noinfep  9651  wemapwe  9688  scott0s  9879  cplem1  9880  karden  9886  acndom2  10045  dfac5lem3  10116  fin23lem31  10334  fin23lem40  10342  isf34lem5  10369  isf34lem7  10370  isf34lem6  10371  axrrecex  11154  negne0bi  11529  rpnnen1lem4  12960  rpnnen1lem5  12961  fseqsupcl  13938  limsupgre  15421  isercolllem3  15609  rpnnen2lem12  16164  ruclem11  16179  3dvds  16270  prmreclem6  16850  0ram  16949  0ram2  16950  0ramcl  16952  gsumval2  18601  ghmrn  19099  gexex  19713  gsumval3  19767  subdrgint  20407  iinopn  22386  cnconn  22908  1stcfb  22931  qtopeu  23202  fbasrn  23370  alexsublem  23530  evth  24457  minveclem1  24923  minveclem3b  24927  ovollb2  24988  ovolunlem1a  24995  ovolunlem1  24996  ovoliunlem1  25001  ovoliun2  25005  ioombl1lem4  25060  uniioombllem1  25080  uniioombllem2  25082  uniioombllem6  25087  mbfsup  25163  mbfinf  25164  mbflimsup  25165  itg1climres  25214  itg2monolem1  25250  itg2mono  25253  itg2i1fseq2  25256  sincos4thpi  26005  nosepnelem  27162  axlowdimlem13  28192  eulerpath  29474  siii  30084  minvecolem1  30105  bcsiALT  30410  h1de2bi  30785  h1de2ctlem  30786  nmlnopgt0i  31228  dimval  32632  dimvalfi  32633  rge0scvg  32867  umgracycusgr  34083  cusgracyclt3v  34085  erdszelem5  34124  cvmsss2  34203  elrn3  34670  rankeq1o  35081  fin2so  36413  heicant  36461  scottn0f  36976  psspwb  40994  fnwe2lem2  41726  sqrtcval  42325