Theorem neeq12d 3005

Description: Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
neeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
neeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
neeq12d	⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

Proof of Theorem neeq12d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		neeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
3	1, 2	eqeq12d 2754	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	necon3bid 2988	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  2nreu  4375  fnelnfp  7049  suppval  7979  infpssrlem4  10062  injresinjlem  13507  sgrp2nmndlem5  18568  pmtr3ncom  19083  isnzr  20530  ptcmplem2  23204  isinag  27199  axlowdimlem6  27315  axlowdimlem14  27323  pthdadjvtx  28098  uhgrwkspthlem2  28122  usgr2wlkspth  28127  usgr2trlncl  28128  pthdlem1  28134  lfgrn1cycl  28170  2wlkdlem5  28294  2pthdlem1  28295  3wlkdlem5  28527  3pthdlem1  28528  numclwwlkovh0  28736  numclwwlk2lem1  28740  numclwlk2lem2f  28741  numclwlk2lem2f1o  28743  eulplig  28847  signsvvfval  32557  signsvfn  32561  bnj1534  32833  bnj1542  32837  bnj1280  33000  derangsn  33132  derangenlem  33133  subfacp1lem3  33144  subfacp1lem5  33146  subfacp1lem6  33147  subfacp1  33148  sltval2  33859  sltres  33865  noseponlem  33867  noextenddif  33871  nosepnelem  33882  nosepeq  33888  nosupbnd2lem1  33918  noinfbnd2lem1  33933  noetasuplem4  33939  noetainflem4  33943  fvtransport  34334  irrdiff  35497  poimirlem1  35778  poimirlem6  35783  poimirlem7  35784  cdlemkid3N  38947  cdlemkid4  38948  sticksstones1  40102  sticksstones2  40103  stoweidlem43  43584  ichnreuop  44924  nnsgrpnmnd  45372  2zrngnmlid  45507  pgrpgt2nabl  45702  ldepsnlinc  45849