Theorem necon3bii 2990

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  necom  2991  neeq1i  3002  neeq2i  3003  neeq12i  3004  rnsnn0  6229  onoviun  8381  onnseq  8382  intrnfi  9453  wdomtr  9612  noinfep  9697  wemapwe  9734  scott0s  9925  cplem1  9926  karden  9932  acndom2  10091  dfac5lem3  10162  fin23lem31  10380  fin23lem40  10388  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  axrrecex  11200  negne0bi  11579  rpnnen1lem4  13019  rpnnen1lem5  13020  fseqsupcl  14014  limsupgre  15513  isercolllem3  15699  rpnnen2lem12  16257  ruclem11  16272  3dvds  16364  prmreclem6  16954  0ram  17053  0ram2  17054  0ramcl  17056  gsumval2  18711  ghmrn  19259  gexex  19885  gsumval3  19939  subdrgint  20820  iinopn  22923  cnconn  23445  1stcfb  23468  qtopeu  23739  fbasrn  23907  alexsublem  24067  evth  25004  minveclem1  25471  minveclem3b  25475  ovollb2  25537  ovolunlem1a  25544  ovolunlem1  25545  ovoliunlem1  25550  ovoliun2  25554  ioombl1lem4  25609  uniioombllem1  25629  uniioombllem2  25631  uniioombllem6  25636  mbfsup  25712  mbfinf  25713  mbflimsup  25714  itg1climres  25763  itg2monolem1  25799  itg2mono  25802  itg2i1fseq2  25805  sincos4thpi  26569  nosepnelem  27738  axlowdimlem13  28983  eulerpath  30269  siii  30881  minvecolem1  30902  bcsiALT  31207  h1de2bi  31582  h1de2ctlem  31583  nmlnopgt0i  32025  wrdpmtrlast  33095  dimval  33627  dimvalfi  33628  rge0scvg  33909  umgracycusgr  35138  cusgracyclt3v  35140  erdszelem5  35179  cvmsss2  35258  elrn3  35741  rankeq1o  36152  fin2so  37593  heicant  37641  scottn0f  38156  psspwb  42245  fnwe2lem2  43039  sqrtcval  43630