Theorem neeq12d 3002

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2940

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  2nreu  4441  fnelnfp  7177  suppval  8150  infpssrlem4  10303  injresinjlem  13756  sgrp2nmndlem5  18846  pmtr3ncom  19384  isnzr  20405  ptcmplem2  23777  sltval2  27383  sltres  27389  noseponlem  27391  noextenddif  27395  nosepnelem  27406  nosepeq  27412  nosupbnd2lem1  27442  noinfbnd2lem1  27457  noetasuplem4  27463  noetainflem4  27467  isinag  28344  axlowdimlem6  28460  axlowdimlem14  28468  pthdadjvtx  29242  uhgrwkspthlem2  29266  usgr2wlkspth  29271  usgr2trlncl  29272  pthdlem1  29278  lfgrn1cycl  29314  2wlkdlem5  29438  2pthdlem1  29439  3wlkdlem5  29671  3pthdlem1  29672  numclwwlkovh0  29880  numclwwlk2lem1  29884  numclwlk2lem2f  29885  numclwlk2lem2f1o  29887  eulplig  29993  opprqusdrng  32869  signsvvfval  33875  signsvfn  33879  bnj1534  34150  bnj1542  34154  bnj1280  34317  derangsn  34447  derangenlem  34448  subfacp1lem3  34459  subfacp1lem5  34461  subfacp1lem6  34462  subfacp1  34463  fvtransport  35296  irrdiff  36510  poimirlem1  36792  poimirlem6  36797  poimirlem7  36798  cdlemkid3N  40107  cdlemkid4  40108  aks6d1c2p2  41263  sticksstones1  41268  sticksstones2  41269  stoweidlem43  45058  ichnreuop  46439  nnsgrpnmnd  46855  2zrngnmlid  46936  pgrpgt2nabl  47131  ldepsnlinc  47277