Theorem necon3bii 3012

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necom  3013  neeq1i  3024  neeq2i  3025  neeq12i  3026  rnsnn0  6198  onoviun  8318  onnseq  8319  intrnfi  9364  wdomtr  9525  noinfep  9617  wemapwe  9654  scott0s  9850  cplem1  9863  karden  9869  acndom2  10026  dfac5lem3  10097  fin23lem31  10315  fin23lem40  10323  isf34lem5  10350  isf34lem7  10351  isf34lem6  10352  axrrecex  11136  negne0bi  11519  rpnnen1lem4  12992  rpnnen1lem5  12993  fseqsupcl  14001  limsupgre  15520  isercolllem3  15706  rpnnen2lem12  16269  ruclem11  16284  3dvds  16377  prmreclem6  16969  0ram  17068  0ram2  17069  0ramcl  17071  gsumval2  18732  ghmrn  19287  gexex  19911  gsumval3  19965  subdrgint  20872  iinopn  23016  cnconn  23536  1stcfb  23559  qtopeu  23830  fbasrn  23998  alexsublem  24158  evth  25075  minveclem1  25540  minveclem3b  25544  ovollb2  25605  ovolunlem1a  25612  ovolunlem1  25613  ovoliunlem1  25618  ovoliun2  25622  ioombl1lem4  25677  uniioombllem1  25697  uniioombllem2  25699  uniioombllem6  25704  mbfsup  25780  mbfinf  25781  mbflimsup  25782  itg1climres  25830  itg2monolem1  25866  itg2mono  25869  itg2i1fseq2  25872  sincos4thpi  26632  nosepnelem  27797  axlowdimlem13  29209  eulerpath  30497  siii  31110  minvecolem1  31131  bcsiALT  31436  h1de2bi  31811  h1de2ctlem  31812  nmlnopgt0i  32254  wrdpmtrlast  33321  dimval  33903  dimvalfi  33904  rge0scvg  34251  umgracycusgr  35512  cusgracyclt3v  35514  erdszelem5  35553  cvmsss2  35632  elrn3  36120  rankeq1o  36529  ttc0elw  36895  ttc0el  36903  regsfromunir1  36908  fin2so  38113  heicant  38161  scottn0f  38676  psspwb  42854  fnwe2lem2  43635  sqrtcval  44224