Theorem necon3bii 2984

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

Syntax hints:  ¬ wn 3   ↔ wb 206   = wceq 1542   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  necom  2985  neeq1i  2996  neeq2i  2997  neeq12i  2998  rnsnn0  6172  onoviun  8283  onnseq  8284  intrnfi  9329  wdomtr  9490  noinfep  9581  wemapwe  9618  scott0s  9812  cplem1  9813  karden  9819  acndom2  9976  dfac5lem3  10047  fin23lem31  10265  fin23lem40  10273  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axrrecex  11086  negne0bi  11467  rpnnen1lem4  12930  rpnnen1lem5  12931  fseqsupcl  13939  limsupgre  15443  isercolllem3  15629  rpnnen2lem12  16192  ruclem11  16207  3dvds  16300  prmreclem6  16892  0ram  16991  0ram2  16992  0ramcl  16994  gsumval2  18654  ghmrn  19204  gexex  19828  gsumval3  19882  subdrgint  20780  iinopn  22867  cnconn  23387  1stcfb  23410  qtopeu  23681  fbasrn  23849  alexsublem  24009  evth  24926  minveclem1  25391  minveclem3b  25395  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun2  25473  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  mbfsup  25631  mbfinf  25632  mbflimsup  25633  itg1climres  25681  itg2monolem1  25717  itg2mono  25720  itg2i1fseq2  25723  sincos4thpi  26477  nosepnelem  27643  axlowdimlem13  29023  eulerpath  30311  siii  30924  minvecolem1  30945  bcsiALT  31250  h1de2bi  31625  h1de2ctlem  31626  nmlnopgt0i  32068  wrdpmtrlast  33154  dimval  33745  dimvalfi  33746  rge0scvg  34093  umgracycusgr  35336  cusgracyclt3v  35338  erdszelem5  35377  cvmsss2  35456  elrn3  35944  rankeq1o  36353  ttc0elw  36709  ttc0el  36717  regsfromunir1  36722  fin2so  37928  heicant  37976  scottn0f  38491  psspwb  42669  fnwe2lem2  43479  sqrtcval  44068