Theorem necon3bii 2995

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

Syntax hints:  ¬ wn 3   ↔ wb 205   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necom  2996  neeq1i  3007  neeq2i  3008  neeq12i  3009  rnsnn0  6100  onoviun  8145  onnseq  8146  intrnfi  9105  wdomtr  9264  noinfep  9348  wemapwe  9385  scott0s  9577  cplem1  9578  karden  9584  acndom2  9741  dfac5lem3  9812  fin23lem31  10030  fin23lem40  10038  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  axrrecex  10850  negne0bi  11224  rpnnen1lem4  12649  rpnnen1lem5  12650  fseqsupcl  13625  limsupgre  15118  isercolllem3  15306  rpnnen2lem12  15862  ruclem11  15877  3dvds  15968  prmreclem6  16550  0ram  16649  0ram2  16650  0ramcl  16652  gsumval2  18285  ghmrn  18762  gexex  19369  gsumval3  19423  subdrgint  19986  iinopn  21959  cnconn  22481  1stcfb  22504  qtopeu  22775  fbasrn  22943  alexsublem  23103  evth  24028  minveclem1  24493  minveclem3b  24497  ovollb2  24558  ovolunlem1a  24565  ovolunlem1  24566  ovoliunlem1  24571  ovoliun2  24575  ioombl1lem4  24630  uniioombllem1  24650  uniioombllem2  24652  uniioombllem6  24657  mbfsup  24733  mbfinf  24734  mbflimsup  24735  itg1climres  24784  itg2monolem1  24820  itg2mono  24823  itg2i1fseq2  24826  sincos4thpi  25575  axlowdimlem13  27225  eulerpath  28506  siii  29116  minvecolem1  29137  bcsiALT  29442  h1de2bi  29817  h1de2ctlem  29818  nmlnopgt0i  30260  dimval  31588  dimvalfi  31589  rge0scvg  31801  umgracycusgr  33016  cusgracyclt3v  33018  erdszelem5  33057  cvmsss2  33136  elrn3  33635  nosepnelem  33809  rankeq1o  34400  fin2so  35691  heicant  35739  scottn0f  36255  psspwb  40129  fnwe2lem2  40792  sqrtcval  41138