Theorem necon3bii 2983

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1534   ≠ wne 2930

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 206  df-ne 2931

This theorem is referenced by:  necom  2984  neeq1i  2995  neeq2i  2996  neeq12i  2997  rnsnn0  6209  onoviun  8362  onnseq  8363  intrnfi  9449  wdomtr  9608  noinfep  9693  wemapwe  9730  scott0s  9921  cplem1  9922  karden  9928  acndom2  10087  dfac5lem3  10158  fin23lem31  10374  fin23lem40  10382  isf34lem5  10409  isf34lem7  10410  isf34lem6  10411  axrrecex  11194  negne0bi  11571  rpnnen1lem4  13007  rpnnen1lem5  13008  fseqsupcl  13988  limsupgre  15475  isercolllem3  15663  rpnnen2lem12  16219  ruclem11  16234  3dvds  16325  prmreclem6  16915  0ram  17014  0ram2  17015  0ramcl  17017  gsumval2  18671  ghmrn  19216  gexex  19844  gsumval3  19898  subdrgint  20775  iinopn  22889  cnconn  23411  1stcfb  23434  qtopeu  23705  fbasrn  23873  alexsublem  24033  evth  24970  minveclem1  25437  minveclem3b  25441  ovollb2  25503  ovolunlem1a  25510  ovolunlem1  25511  ovoliunlem1  25516  ovoliun2  25520  ioombl1lem4  25575  uniioombllem1  25595  uniioombllem2  25597  uniioombllem6  25602  mbfsup  25678  mbfinf  25679  mbflimsup  25680  itg1climres  25729  itg2monolem1  25765  itg2mono  25768  itg2i1fseq2  25771  sincos4thpi  26535  nosepnelem  27703  axlowdimlem13  28882  eulerpath  30168  siii  30780  minvecolem1  30801  bcsiALT  31106  h1de2bi  31481  h1de2ctlem  31482  nmlnopgt0i  31924  wrdpmtrlast  32972  dimval  33498  dimvalfi  33499  rge0scvg  33774  umgracycusgr  34992  cusgracyclt3v  34994  erdszelem5  35033  cvmsss2  35112  elrn3  35594  rankeq1o  36005  fin2so  37318  heicant  37366  scottn0f  37881  psspwb  41969  fnwe2lem2  42746  sqrtcval  43342