Theorem neeq12d 3048

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  2nreu  4349  fnelnfp  6916  suppval  7815  infpssrlem4  9717  injresinjlem  13152  sgrp2nmndlem5  18086  pmtr3ncom  18595  isnzr  20025  ptcmplem2  22658  isinag  26632  axlowdimlem6  26741  axlowdimlem14  26749  pthdadjvtx  27519  uhgrwkspthlem2  27543  usgr2wlkspth  27548  usgr2trlncl  27549  pthdlem1  27555  lfgrn1cycl  27591  2wlkdlem5  27715  2pthdlem1  27716  3wlkdlem5  27948  3pthdlem1  27949  numclwwlkovh0  28157  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  eulplig  28268  signsvvfval  31958  signsvfn  31962  bnj1534  32235  bnj1542  32239  bnj1280  32402  derangsn  32530  derangenlem  32531  subfacp1lem3  32542  subfacp1lem5  32544  subfacp1lem6  32545  subfacp1  32546  sltval2  33276  sltres  33282  noseponlem  33284  noextenddif  33288  nosepnelem  33297  nosepeq  33302  nosupbnd2lem1  33328  noetalem3  33332  fvtransport  33606  irrdiff  34740  poimirlem1  35058  poimirlem6  35063  poimirlem7  35064  cdlemkid3N  38229  cdlemkid4  38230  stoweidlem43  42685  ichnreuop  43989  nnsgrpnmnd  44438  2zrngnmlid  44573  pgrpgt2nabl  44768  ldepsnlinc  44917