Theorem neeq12d 3003

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 2749	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷))
4	3	necon3bid 2986	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  2nreu  4442  fnelnfp  7175  suppval  8148  infpssrlem4  10301  injresinjlem  13752  sgrp2nmndlem5  18810  pmtr3ncom  19343  isnzr  20293  ptcmplem2  23557  sltval2  27159  sltres  27165  noseponlem  27167  noextenddif  27171  nosepnelem  27182  nosepeq  27188  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem4  27239  noetainflem4  27243  isinag  28089  axlowdimlem6  28205  axlowdimlem14  28213  pthdadjvtx  28987  uhgrwkspthlem2  29011  usgr2wlkspth  29016  usgr2trlncl  29017  pthdlem1  29023  lfgrn1cycl  29059  2wlkdlem5  29183  2pthdlem1  29184  3wlkdlem5  29416  3pthdlem1  29417  numclwwlkovh0  29625  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  eulplig  29738  opprqusdrng  32607  signsvvfval  33589  signsvfn  33593  bnj1534  33864  bnj1542  33868  bnj1280  34031  derangsn  34161  derangenlem  34162  subfacp1lem3  34173  subfacp1lem5  34175  subfacp1lem6  34176  subfacp1  34177  fvtransport  35004  irrdiff  36207  poimirlem1  36489  poimirlem6  36494  poimirlem7  36495  cdlemkid3N  39804  cdlemkid4  39805  aks6d1c2p2  40957  sticksstones1  40962  sticksstones2  40963  stoweidlem43  44759  ichnreuop  46140  nnsgrpnmnd  46588  2zrngnmlid  46847  pgrpgt2nabl  47042  ldepsnlinc  47189