Theorem neeq12d 2986

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  2nreu  4397  fnelnfp  7117  2f1fvneq  7201  resf1extb  7874  suppval  8102  infpssrlem4  10219  injresinjlem  13708  sgrp2nmndlem5  18821  pmtr3ncom  19372  isnzr  20417  nzrpropd  20423  ptcmplem2  23956  sltval2  27584  sltres  27590  noseponlem  27592  noextenddif  27596  nosepnelem  27607  nosepeq  27613  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem4  27664  noetainflem4  27668  isinag  28801  axlowdimlem6  28910  axlowdimlem14  28918  pthdadjvtx  29691  uhgrwkspthlem2  29717  usgr2wlkspth  29722  usgr2trlncl  29723  pthdlem1  29729  lfgrn1cycl  29768  2wlkdlem5  29892  2pthdlem1  29893  3wlkdlem5  30125  3pthdlem1  30126  numclwwlkovh0  30334  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  eulplig  30447  opprqusdrng  33440  signsvvfval  34545  signsvfn  34549  bnj1534  34819  bnj1542  34823  bnj1280  34986  derangsn  35142  derangenlem  35143  subfacp1lem3  35154  subfacp1lem5  35156  subfacp1lem6  35157  subfacp1  35158  fvtransport  36005  irrdiff  37299  poimirlem1  37600  poimirlem6  37605  poimirlem7  37606  cdlemkid3N  40912  cdlemkid4  40913  aks6d1c2p2  42092  hashscontpow  42095  sticksstones1  42119  sticksstones2  42120  stoweidlem43  46025  modm1nem2  47354  ichnreuop  47457  upgrimpthslem2  47893  isubgr3stgrlem4  47954  gpg5nbgrvtx13starlem2  48057  gpgprismgr4cycllem7  48086  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem4  48104  pgnbgreunbgrlem5  48108  nnsgrpnmnd  48163  2zrngnmlid  48240  pgrpgt2nabl  48351  ldepsnlinc  48494