Theorem neeq12d 2855

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  fnelnfp  6443  suppval  7297  infpssrlem4  9128  injresinjlem  12588  sgrp2nmndlem5  17416  pmtr3ncom  17895  isnzr  19259  ptcmplem2  21857  isinag  25729  axlowdimlem6  25827  axlowdimlem14  25835  pthdadjvtx  26626  uhgrwkspthlem2  26650  usgr2wlkspth  26655  usgr2trlncl  26656  pthdlem1  26662  lfgrn1cycl  26697  2wlkdlem5  26825  2pthdlem1  26826  3wlkdlem5  27023  3pthdlem1  27024  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  eulplig  27337  signsvvfval  30655  signsvfn  30659  bnj1534  30923  bnj1542  30927  bnj1280  31088  derangsn  31152  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  subfacp1lem6  31167  subfacp1  31168  sltval2  31809  sltres  31815  noseponlem  31817  noextenddif  31821  nosepnelem  31830  nosepeq  31835  nosupbnd2lem1  31861  noetalem3  31865  fvtransport  32139  poimirlem1  33410  poimirlem6  33415  poimirlem7  33416  cdlemkid3N  36221  cdlemkid4  36222  stoweidlem43  40260  nnsgrpnmnd  41818  2zrngnmlid  41949  pgrpgt2nabl  42147  ldepsnlinc  42297