Theorem necon3bii 3008

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

Syntax hints:  ¬ wn 3   ↔ wb 208   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necom  3009  neeq1i  3020  neeq2i  3021  neeq12i  3022  rnsnn0  6191  onoviun  8309  onnseq  8310  intrnfi  9359  wdomtr  9520  noinfep  9612  wemapwe  9649  scott0s  9843  cplem1  9844  karden  9850  acndom2  10007  dfac5lem3  10078  fin23lem31  10297  fin23lem40  10305  isf34lem5  10332  isf34lem7  10333  isf34lem6  10334  axrrecex  11118  negne0bi  11501  rpnnen1lem4  12978  rpnnen1lem5  12979  fseqsupcl  13987  limsupgre  15491  isercolllem3  15677  rpnnen2lem12  16240  ruclem11  16255  3dvds  16348  prmreclem6  16940  0ram  17039  0ram2  17040  0ramcl  17042  gsumval2  18703  ghmrn  19252  gexex  19876  gsumval3  19930  subdrgint  20832  iinopn  22942  cnconn  23462  1stcfb  23485  qtopeu  23756  fbasrn  23924  alexsublem  24084  evth  25001  minveclem1  25466  minveclem3b  25470  ovollb2  25531  ovolunlem1a  25538  ovolunlem1  25539  ovoliunlem1  25544  ovoliun2  25548  ioombl1lem4  25603  uniioombllem1  25623  uniioombllem2  25625  uniioombllem6  25630  mbfsup  25706  mbfinf  25707  mbflimsup  25708  itg1climres  25756  itg2monolem1  25792  itg2mono  25795  itg2i1fseq2  25798  sincos4thpi  26555  nosepnelem  27720  axlowdimlem13  29101  eulerpath  30389  siii  31002  minvecolem1  31023  bcsiALT  31328  h1de2bi  31703  h1de2ctlem  31704  nmlnopgt0i  32146  wrdpmtrlast  33234  dimval  33859  dimvalfi  33860  rge0scvg  34207  umgracycusgr  35468  cusgracyclt3v  35470  erdszelem5  35509  cvmsss2  35588  elrn3  36076  rankeq1o  36485  ttc0elw  36851  ttc0el  36859  regsfromunir1  36864  fin2so  38070  heicant  38118  scottn0f  38633  psspwb  42811  fnwe2lem2  43592  sqrtcval  44181