Theorem neeq12d 3019

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  2nreu  4410  fnelnfp  7177  2f1fvneq  7260  resf1extb  7932  suppval  8159  infpssrlem4  10291  injresinjlem  13821  sgrp2nmndlem5  18992  pmtr3ncom  19546  isnzr  20598  nzrpropd  20605  ptcmplem2  24191  ltsval2  27798  ltsres  27804  noseponlem  27806  noextenddif  27810  nosepnelem  27821  nosepeq  27827  nosupbnd2lem1  27857  noinfbnd2lem1  27872  noetasuplem4  27878  noetainflem4  27882  isinag  29133  axlowdimlem6  29275  axlowdimlem14  29283  pthdadjvtx  30055  uhgrwkspthlem2  30081  usgr2wlkspth  30086  usgr2trlncl  30087  pthdlem1  30093  lfgrn1cycl  30132  2wlkdlem5  30256  2pthdlem1  30257  3wlkdlem5  30492  3pthdlem1  30493  numclwwlkovh0  30701  numclwwlk2lem1  30705  numclwlk2lem2f  30706  numclwlk2lem2f1o  30708  eulplig  30815  opprqusdrng  33753  signsvvfval  34943  signsvfn  34947  bnj1534  35219  bnj1542  35223  bnj1280  35386  derangsn  35640  derangenlem  35641  subfacp1lem3  35652  subfacp1lem5  35654  subfacp1lem6  35655  subfacp1  35656  fvtransport  36502  mh-inf3f1  37030  irrdiff  37948  poimirlem1  38250  poimirlem6  38255  poimirlem7  38256  cdlemkid3N  41685  cdlemkid4  41686  aks6d1c2p2  42864  hashscontpow  42867  sticksstones1  42891  sticksstones2  42892  stoweidlem43  46737  modm1nem2  48089  ichnreuop  48198  upgrimpthslem2  48650  isubgr3stgrlem4  48711  gpg5nbgrvtx13starlem2  48814  gpgprismgr4cycllem7  48843  pgnbgreunbgrlem1  48855  pgnbgreunbgrlem4  48861  pgnbgreunbgrlem5  48865  nnsgrpnmnd  48920  2zrngnmlid  48997  pgrpgt2nabl  49123  ldepsnlinc  49265