Theorem necon3bii 3011

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  necom  3012  neeq1i  3023  neeq2i  3024  neeq12i  3025  rnsnn0  6223  onoviun  8382  onnseq  8383  intrnfi  9438  wdomtr  9599  noinfep  9691  wemapwe  9728  scott0bs  9974  scott0bsOLD  9975  cplem1  9980  cplem1OLD  9981  karden  9989  kardenOLD  9990  acndom2  10163  dfac5lem3  10234  fin23lem31  10451  fin23lem40  10459  isf34lem5  10486  isf34lem7  10487  isf34lem6  10488  axrrecex  11278  negne0bi  11661  rpnnen1lem4  13138  rpnnen1lem5  13139  fseqsupcl  14150  limsupgre  15680  isercolllem3  15866  rpnnen2lem12  16425  ruclem11  16440  3dvds  16533  prmreclem6  17131  0ram  17230  0ram2  17231  0ramcl  17233  gsumval2  18907  ghmrn  19475  gexex  20100  gsumval3  20154  subdrgint  21093  iinopn  23253  cnconn  23773  1stcfb  23796  qtopeu  24068  fbasrn  24236  alexsublem  24396  evth  25313  minveclem1  25778  minveclem3b  25782  ovollb2  25843  ovolunlem1a  25850  ovolunlem1  25851  ovoliunlem1  25856  ovoliun2  25860  ioombl1lem4  25915  uniioombllem1  25935  uniioombllem2  25937  uniioombllem6  25942  mbfsup  26018  mbfinf  26019  mbflimsup  26020  itg1climres  26068  itg2monolem1  26104  itg2mono  26107  itg2i1fseq2  26110  sincos4thpi  26875  nosepnelem  28069  axlowdimlem13  29565  eulerpath  30875  siii  31488  minvecolem1  31509  bcsiALT  31814  h1de2bi  32189  h1de2ctlem  32190  nmlnopgt0i  32632  wrdpmtrlast  33730  dimval  34316  dimvalfi  34317  rge0scvg  34664  elscottn0  35849  rankscott  35851  ecscottd  35857  kardeq0  35937  umgracycusgr  36089  cusgracyclt3v  36091  erdszelem5  36140  cvmsss2  36219  elrn3  36718  rankeq1o  37123  ttc0elw  37506  ttc0el  37514  regsfromunir1  37519  fin2so  38735  heicant  38778  scottn0f  39305  psspwb  43486  sqrtcval  44844