Theorem necon3bii 3012

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

Syntax hints:  ¬ wn 3   ↔ wb 209   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necom  3013  neeq1i  3024  neeq2i  3025  neeq12i  3026  rnsnn0  6199  onoviun  8318  onnseq  8319  intrnfi  9364  wdomtr  9525  noinfep  9617  wemapwe  9654  scott0s  9850  cplem1  9863  karden  9869  acndom2  10026  dfac5lem3  10097  fin23lem31  10315  fin23lem40  10323  isf34lem5  10350  isf34lem7  10351  isf34lem6  10352  axrrecex  11136  negne0bi  11519  rpnnen1lem4  12995  rpnnen1lem5  12996  fseqsupcl  14004  limsupgre  15522  isercolllem3  15708  rpnnen2lem12  16271  ruclem11  16286  3dvds  16379  prmreclem6  16971  0ram  17070  0ram2  17071  0ramcl  17073  gsumval2  18734  ghmrn  19290  gexex  19914  gsumval3  19968  subdrgint  20875  iinopn  23020  cnconn  23540  1stcfb  23563  qtopeu  23834  fbasrn  24002  alexsublem  24162  evth  25079  minveclem1  25544  minveclem3b  25548  ovollb2  25609  ovolunlem1a  25616  ovolunlem1  25617  ovoliunlem1  25622  ovoliun2  25626  ioombl1lem4  25681  uniioombllem1  25701  uniioombllem2  25703  uniioombllem6  25708  mbfsup  25784  mbfinf  25785  mbflimsup  25786  itg1climres  25834  itg2monolem1  25870  itg2mono  25873  itg2i1fseq2  25876  sincos4thpi  26636  nosepnelem  27801  axlowdimlem13  29213  eulerpath  30501  siii  31114  minvecolem1  31135  bcsiALT  31440  h1de2bi  31815  h1de2ctlem  31816  nmlnopgt0i  32258  wrdpmtrlast  33326  dimval  33908  dimvalfi  33909  rge0scvg  34256  umgracycusgr  35517  cusgracyclt3v  35519  erdszelem5  35558  cvmsss2  35637  elrn3  36125  rankeq1o  36534  ttc0elw  36900  ttc0el  36908  regsfromunir1  36913  fin2so  38118  heicant  38166  scottn0f  38681  psspwb  42859  fnwe2lem2  43640  sqrtcval  44229