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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  2nreu  4444  fnelnfp  7197  resf1extb  7956  suppval  8187  infpssrlem4  10346  injresinjlem  13826  sgrp2nmndlem5  18942  pmtr3ncom  19493  isnzr  20514  nzrpropd  20520  ptcmplem2  24061  sltval2  27701  sltres  27707  noseponlem  27709  noextenddif  27713  nosepnelem  27724  nosepeq  27730  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  isinag  28846  axlowdimlem6  28962  axlowdimlem14  28970  pthdadjvtx  29748  uhgrwkspthlem2  29774  usgr2wlkspth  29779  usgr2trlncl  29780  pthdlem1  29786  lfgrn1cycl  29825  2wlkdlem5  29949  2pthdlem1  29950  3wlkdlem5  30182  3pthdlem1  30183  numclwwlkovh0  30391  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  eulplig  30504  opprqusdrng  33521  signsvvfval  34593  signsvfn  34597  bnj1534  34867  bnj1542  34871  bnj1280  35034  derangsn  35175  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  subfacp1  35191  fvtransport  36033  irrdiff  37327  poimirlem1  37628  poimirlem6  37633  poimirlem7  37634  cdlemkid3N  40935  cdlemkid4  40936  aks6d1c2p2  42120  hashscontpow  42123  sticksstones1  42147  sticksstones2  42148  stoweidlem43  46058  ichnreuop  47459  isubgr3stgrlem4  47936  gpg5nbgrvtx13starlem2  48028  nnsgrpnmnd  48094  2zrngnmlid  48171  pgrpgt2nabl  48282  ldepsnlinc  48425