Theorem necon3bii 3009

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

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

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 2958

This theorem is used by:  necom  3010  neeq1i  3021  neeq2i  3022  neeq12i  3023  rnsnn0  6208  onoviun  8336  onnseq  8337  intrnfi  9390  wdomtr  9551  noinfep  9643  wemapwe  9680  scott0bs  9887  scott0bsOLD  9888  cplem1  9893  cplem1OLD  9894  karden  9902  kardenOLD  9903  acndom2  10061  dfac5lem3  10132  fin23lem31  10349  fin23lem40  10357  isf34lem5  10384  isf34lem7  10385  isf34lem6  10386  axrrecex  11176  negne0bi  11559  rpnnen1lem4  13034  rpnnen1lem5  13035  fseqsupcl  14045  limsupgre  15572  isercolllem3  15758  rpnnen2lem12  16319  ruclem11  16334  3dvds  16427  prmreclem6  17019  0ram  17118  0ram2  17119  0ramcl  17121  gsumval2  18794  ghmrn  19362  gexex  19986  gsumval3  20040  subdrgint  20975  iinopn  23133  cnconn  23653  1stcfb  23676  qtopeu  23948  fbasrn  24116  alexsublem  24276  evth  25193  minveclem1  25658  minveclem3b  25662  ovollb2  25723  ovolunlem1a  25730  ovolunlem1  25731  ovoliunlem1  25736  ovoliun2  25740  ioombl1lem4  25795  uniioombllem1  25815  uniioombllem2  25817  uniioombllem6  25822  mbfsup  25898  mbfinf  25899  mbflimsup  25900  itg1climres  25948  itg2monolem1  25984  itg2mono  25987  itg2i1fseq2  25990  sincos4thpi  26758  nosepnelem  27923  axlowdimlem13  29419  eulerpath  30729  siii  31342  minvecolem1  31363  bcsiALT  31668  h1de2bi  32043  h1de2ctlem  32044  nmlnopgt0i  32486  wrdpmtrlast  33541  dimval  34119  dimvalfi  34120  rge0scvg  34467  rankscott  35643  kardeq0  35690  umgracycusgr  35741  cusgracyclt3v  35743  erdszelem5  35782  cvmsss2  35861  elrn3  36349  rankeq1o  36759  ttc0elw  37154  ttc0el  37162  regsfromunir1  37167  fin2so  38369  heicant  38412  scottn0f  38926  psspwb  43106  fnwe2lem2  43900  sqrtcval  44489