Theorem necon3bii 2981

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 207  df-ne 2930

This theorem is referenced by:  necom  2982  neeq1i  2993  neeq2i  2994  neeq12i  2995  rnsnn0  6160  onoviun  8269  onnseq  8270  intrnfi  9307  wdomtr  9468  noinfep  9557  wemapwe  9594  scott0s  9788  cplem1  9789  karden  9795  acndom2  9952  dfac5lem3  10023  fin23lem31  10241  fin23lem40  10249  isf34lem5  10276  isf34lem7  10277  isf34lem6  10278  axrrecex  11061  negne0bi  11441  rpnnen1lem4  12880  rpnnen1lem5  12881  fseqsupcl  13886  limsupgre  15390  isercolllem3  15576  rpnnen2lem12  16136  ruclem11  16151  3dvds  16244  prmreclem6  16835  0ram  16934  0ram2  16935  0ramcl  16937  gsumval2  18596  ghmrn  19143  gexex  19767  gsumval3  19821  subdrgint  20720  iinopn  22818  cnconn  23338  1stcfb  23361  qtopeu  23632  fbasrn  23800  alexsublem  23960  evth  24886  minveclem1  25352  minveclem3b  25356  ovollb2  25418  ovolunlem1a  25425  ovolunlem1  25426  ovoliunlem1  25431  ovoliun2  25435  ioombl1lem4  25490  uniioombllem1  25510  uniioombllem2  25512  uniioombllem6  25517  mbfsup  25593  mbfinf  25594  mbflimsup  25595  itg1climres  25643  itg2monolem1  25679  itg2mono  25682  itg2i1fseq2  25685  sincos4thpi  26450  nosepnelem  27619  axlowdimlem13  28934  eulerpath  30223  siii  30835  minvecolem1  30856  bcsiALT  31161  h1de2bi  31536  h1de2ctlem  31537  nmlnopgt0i  31979  wrdpmtrlast  33069  dimval  33634  dimvalfi  33635  rge0scvg  33983  umgracycusgr  35219  cusgracyclt3v  35221  erdszelem5  35260  cvmsss2  35339  elrn3  35827  rankeq1o  36236  fin2so  37668  heicant  37716  scottn0f  38231  psspwb  42347  fnwe2lem2  43169  sqrtcval  43759