Theorem neeq12d 2993

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  2nreu  4396  fnelnfp  7123  2f1fvneq  7206  resf1extb  7876  suppval  8104  infpssrlem4  10216  injresinjlem  13706  sgrp2nmndlem5  18854  pmtr3ncom  19404  isnzr  20447  nzrpropd  20453  ptcmplem2  23997  ltsval2  27624  ltsres  27630  noseponlem  27632  noextenddif  27636  nosepnelem  27647  nosepeq  27653  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  isinag  28910  axlowdimlem6  29020  axlowdimlem14  29028  pthdadjvtx  29801  uhgrwkspthlem2  29827  usgr2wlkspth  29832  usgr2trlncl  29833  pthdlem1  29839  lfgrn1cycl  29878  2wlkdlem5  30002  2pthdlem1  30003  3wlkdlem5  30238  3pthdlem1  30239  numclwwlkovh0  30447  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  eulplig  30560  opprqusdrng  33574  signsvvfval  34735  signsvfn  34739  bnj1534  35009  bnj1542  35013  bnj1280  35176  derangsn  35364  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  subfacp1  35380  fvtransport  36226  irrdiff  37527  poimirlem1  37818  poimirlem6  37823  poimirlem7  37824  cdlemkid3N  41189  cdlemkid4  41190  aks6d1c2p2  42369  hashscontpow  42372  sticksstones1  42396  sticksstones2  42397  stoweidlem43  46283  modm1nem2  47611  ichnreuop  47714  upgrimpthslem2  48150  isubgr3stgrlem4  48211  gpg5nbgrvtx13starlem2  48314  gpgprismgr4cycllem7  48343  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5  48365  nnsgrpnmnd  48420  2zrngnmlid  48497  pgrpgt2nabl  48608  ldepsnlinc  48750