Theorem necon3bii 3021

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

Syntax hints:  ¬ wn 3   ↔ wb 198   = wceq 1601   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  necom  3022  neeq1i  3033  neeq2i  3034  neeq12i  3035  rnsnn0  5857  onoviun  7725  onnseq  7726  intrnfi  8612  wdomtr  8771  noinfep  8856  wemapwe  8893  scott0s  9050  cplem1  9051  karden  9057  acndom2  9212  dfac5lem3  9283  fin23lem31  9502  fin23lem40  9510  isf34lem5  9537  isf34lem7  9538  isf34lem6  9539  axrrecex  10322  negne0bi  10698  rpnnen1lem4  12132  rpnnen1lem5  12133  fseqsupcl  13100  limsupgre  14629  isercolllem3  14814  rpnnen2lem12  15367  ruclem11  15382  3dvds  15469  prmreclem6  16040  0ram  16139  0ram2  16140  0ramcl  16142  gsumval2  17677  ghmrn  18068  gexex  18653  gsumval3  18705  iinopn  21125  cnconn  21645  1stcfb  21668  qtopeu  21939  fbasrn  22107  alexsublem  22267  evth  23177  minveclem1  23641  minveclem3b  23645  ovollb2  23704  ovolunlem1a  23711  ovolunlem1  23712  ovoliunlem1  23717  ovoliun2  23721  ioombl1lem4  23776  uniioombllem1  23796  uniioombllem2  23798  uniioombllem6  23803  mbfsup  23879  mbfinf  23880  mbflimsup  23881  itg1climres  23929  itg2monolem1  23965  itg2mono  23968  itg2i1fseq2  23971  sincos4thpi  24714  axlowdimlem13  26320  eulerpath  27662  siii  28297  minvecolem1  28319  bcsiALT  28625  h1de2bi  29002  h1de2ctlem  29003  nmlnopgt0i  29445  dimval  30429  dimvalfi  30430  rge0scvg  30601  erdszelem5  31784  cvmsss2  31863  elrn3  32254  nosepnelem  32427  rankeq1o  32875  fin2so  34030  heicant  34079  scottn0f  34610  psspwb  38136  fnwe2lem2  38594  wnefimgd  39430