Theorem necon3bii 2985

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necom  2986  neeq1i  2997  neeq2i  2998  neeq12i  2999  rnsnn0  6174  onoviun  8285  onnseq  8286  intrnfi  9331  wdomtr  9492  noinfep  9581  wemapwe  9618  scott0s  9812  cplem1  9813  karden  9819  acndom2  9976  dfac5lem3  10047  fin23lem31  10265  fin23lem40  10273  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axrrecex  11086  negne0bi  11466  rpnnen1lem4  12905  rpnnen1lem5  12906  fseqsupcl  13912  limsupgre  15416  isercolllem3  15602  rpnnen2lem12  16162  ruclem11  16177  3dvds  16270  prmreclem6  16861  0ram  16960  0ram2  16961  0ramcl  16963  gsumval2  18623  ghmrn  19170  gexex  19794  gsumval3  19848  subdrgint  20748  iinopn  22858  cnconn  23378  1stcfb  23401  qtopeu  23672  fbasrn  23840  alexsublem  24000  evth  24926  minveclem1  25392  minveclem3b  25396  ovollb2  25458  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun2  25475  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem2  25552  uniioombllem6  25557  mbfsup  25633  mbfinf  25634  mbflimsup  25635  itg1climres  25683  itg2monolem1  25719  itg2mono  25722  itg2i1fseq2  25725  sincos4thpi  26490  nosepnelem  27659  axlowdimlem13  29039  eulerpath  30328  siii  30940  minvecolem1  30961  bcsiALT  31266  h1de2bi  31641  h1de2ctlem  31642  nmlnopgt0i  32084  wrdpmtrlast  33186  dimval  33777  dimvalfi  33778  rge0scvg  34126  umgracycusgr  35367  cusgracyclt3v  35369  erdszelem5  35408  cvmsss2  35487  elrn3  35975  rankeq1o  36384  regsfromunir1  36689  fin2so  37855  heicant  37903  scottn0f  38418  psspwb  42597  fnwe2lem2  43405  sqrtcval  43994