Theorem neeq12d 3008

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  2nreu  4467  fnelnfp  7211  suppval  8203  infpssrlem4  10375  injresinjlem  13837  sgrp2nmndlem5  18964  pmtr3ncom  19517  isnzr  20540  nzrpropd  20546  ptcmplem2  24082  sltval2  27719  sltres  27725  noseponlem  27727  noextenddif  27731  nosepnelem  27742  nosepeq  27748  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  noetainflem4  27803  isinag  28864  axlowdimlem6  28980  axlowdimlem14  28988  pthdadjvtx  29766  uhgrwkspthlem2  29790  usgr2wlkspth  29795  usgr2trlncl  29796  pthdlem1  29802  lfgrn1cycl  29838  2wlkdlem5  29962  2pthdlem1  29963  3wlkdlem5  30195  3pthdlem1  30196  numclwwlkovh0  30404  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  eulplig  30517  opprqusdrng  33486  signsvvfval  34555  signsvfn  34559  bnj1534  34829  bnj1542  34833  bnj1280  34996  derangsn  35138  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  subfacp1  35154  fvtransport  35996  irrdiff  37292  poimirlem1  37581  poimirlem6  37586  poimirlem7  37587  cdlemkid3N  40890  cdlemkid4  40891  aks6d1c2p2  42076  hashscontpow  42079  sticksstones1  42103  sticksstones2  42104  stoweidlem43  45964  ichnreuop  47346  nnsgrpnmnd  47901  2zrngnmlid  47978  pgrpgt2nabl  48091  ldepsnlinc  48237