Theorem necon3bii 3013

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

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

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 2962

This theorem is used by:  necom  3014  neeq1i  3025  neeq2i  3026  neeq12i  3027  rnsnn0  6214  onoviun  8339  onnseq  8340  intrnfi  9386  wdomtr  9547  noinfep  9639  wemapwe  9676  scott0bs  9883  scott0bsOLD  9884  cplem1  9889  cplem1OLD  9890  karden  9898  kardenOLD  9899  acndom2  10057  dfac5lem3  10128  fin23lem31  10345  fin23lem40  10353  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  axrrecex  11166  negne0bi  11549  rpnnen1lem4  13022  rpnnen1lem5  13023  fseqsupcl  14033  limsupgre  15558  isercolllem3  15744  rpnnen2lem12  16306  ruclem11  16321  3dvds  16414  prmreclem6  17006  0ram  17105  0ram2  17106  0ramcl  17108  gsumval2  18773  ghmrn  19330  gexex  19954  gsumval3  20008  subdrgint  20943  iinopn  23096  cnconn  23616  1stcfb  23639  qtopeu  23910  fbasrn  24078  alexsublem  24238  evth  25155  minveclem1  25620  minveclem3b  25624  ovollb2  25685  ovolunlem1a  25692  ovolunlem1  25693  ovoliunlem1  25698  ovoliun2  25702  ioombl1lem4  25757  uniioombllem1  25777  uniioombllem2  25779  uniioombllem6  25784  mbfsup  25860  mbfinf  25861  mbflimsup  25862  itg1climres  25910  itg2monolem1  25946  itg2mono  25949  itg2i1fseq2  25952  sincos4thpi  26715  nosepnelem  27880  axlowdimlem13  29341  eulerpath  30629  siii  31242  minvecolem1  31263  bcsiALT  31568  h1de2bi  31943  h1de2ctlem  31944  nmlnopgt0i  32386  wrdpmtrlast  33444  dimval  34022  dimvalfi  34023  rge0scvg  34370  rankscott  35546  kardeq0  35593  umgracycusgr  35667  cusgracyclt3v  35669  erdszelem5  35708  cvmsss2  35787  elrn3  36275  rankeq1o  36684  ttc0elw  37079  ttc0el  37087  regsfromunir1  37092  fin2so  38299  heicant  38347  scottn0f  38860  psspwb  43040  fnwe2lem2  43819  sqrtcval  44408