Theorem necon3bii 3010

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necom  3011  neeq1i  3022  neeq2i  3023  neeq12i  3024  rnsnn0  6211  onoviun  8331  onnseq  8332  intrnfi  9377  wdomtr  9538  noinfep  9630  wemapwe  9667  scott0s  9863  cplem1  9876  karden  9882  acndom2  10039  dfac5lem3  10110  fin23lem31  10328  fin23lem40  10336  isf34lem5  10363  isf34lem7  10364  isf34lem6  10365  axrrecex  11149  negne0bi  11532  rpnnen1lem4  13005  rpnnen1lem5  13006  fseqsupcl  14015  limsupgre  15534  isercolllem3  15720  rpnnen2lem12  16282  ruclem11  16297  3dvds  16390  prmreclem6  16982  0ram  17081  0ram2  17082  0ramcl  17084  gsumval2  18745  ghmrn  19300  gexex  19924  gsumval3  19978  subdrgint  20887  iinopn  23040  cnconn  23560  1stcfb  23583  qtopeu  23854  fbasrn  24022  alexsublem  24182  evth  25099  minveclem1  25564  minveclem3b  25568  ovollb2  25629  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliun2  25646  ioombl1lem4  25701  uniioombllem1  25721  uniioombllem2  25723  uniioombllem6  25728  mbfsup  25804  mbfinf  25805  mbflimsup  25806  itg1climres  25854  itg2monolem1  25890  itg2mono  25893  itg2i1fseq2  25896  sincos4thpi  26659  nosepnelem  27824  axlowdimlem13  29285  eulerpath  30573  siii  31186  minvecolem1  31207  bcsiALT  31512  h1de2bi  31887  h1de2ctlem  31888  nmlnopgt0i  32330  wrdpmtrlast  33394  dimval  33972  dimvalfi  33973  rge0scvg  34320  rankscott  35503  kardeq0  35550  umgracycusgr  35627  cusgracyclt3v  35629  erdszelem5  35668  cvmsss2  35747  elrn3  36235  rankeq1o  36644  ttc0elw  37019  ttc0el  37027  regsfromunir1  37032  fin2so  38239  heicant  38287  scottn0f  38800  psspwb  42980  fnwe2lem2  43761  sqrtcval  44350