Theorem necon3bii 3007

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

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

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 2956

This theorem is used by:  necom  3008  neeq1i  3019  neeq2i  3020  neeq12i  3021  rnsnn0  6209  onoviun  8354  onnseq  8355  intrnfi  9411  wdomtr  9572  noinfep  9664  wemapwe  9701  scott0bs  9947  scott0bsOLD  9948  cplem1  9953  cplem1OLD  9954  karden  9962  kardenOLD  9963  acndom2  10136  dfac5lem3  10207  fin23lem31  10424  fin23lem40  10432  isf34lem5  10459  isf34lem7  10460  isf34lem6  10461  axrrecex  11251  negne0bi  11634  rpnnen1lem4  13111  rpnnen1lem5  13112  fseqsupcl  14123  limsupgre  15653  isercolllem3  15839  rpnnen2lem12  16398  ruclem11  16413  3dvds  16506  prmreclem6  17104  0ram  17203  0ram2  17204  0ramcl  17206  gsumval2  18880  ghmrn  19448  gexex  20072  gsumval3  20126  subdrgint  21065  iinopn  23225  cnconn  23745  1stcfb  23768  qtopeu  24040  fbasrn  24208  alexsublem  24368  evth  25285  minveclem1  25750  minveclem3b  25754  ovollb2  25815  ovolunlem1a  25822  ovolunlem1  25823  ovoliunlem1  25828  ovoliun2  25832  ioombl1lem4  25887  uniioombllem1  25907  uniioombllem2  25909  uniioombllem6  25914  mbfsup  25990  mbfinf  25991  mbflimsup  25992  itg1climres  26040  itg2monolem1  26076  itg2mono  26079  itg2i1fseq2  26082  sincos4thpi  26847  nosepnelem  28041  axlowdimlem13  29537  eulerpath  30847  siii  31460  minvecolem1  31481  bcsiALT  31786  h1de2bi  32161  h1de2ctlem  32162  nmlnopgt0i  32604  wrdpmtrlast  33700  dimval  34279  dimvalfi  34280  rge0scvg  34627  rankscott  35806  kardeq0  35880  umgracycusgr  35995  cusgracyclt3v  35997  erdszelem5  36046  cvmsss2  36125  elrn3  36619  rankeq1o  37024  ttc0elw  37407  ttc0el  37415  regsfromunir1  37420  fin2so  38623  heicant  38666  scottn0f  39195  psspwb  43375  sqrtcval  44734