Theorem neeq12d 2987

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

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

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 2702

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

This theorem is referenced by:  2nreu  4409  fnelnfp  7153  2f1fvneq  7237  resf1extb  7912  suppval  8143  infpssrlem4  10265  injresinjlem  13754  sgrp2nmndlem5  18862  pmtr3ncom  19411  isnzr  20429  nzrpropd  20435  ptcmplem2  23946  sltval2  27574  sltres  27580  noseponlem  27582  noextenddif  27586  nosepnelem  27597  nosepeq  27603  nosupbnd2lem1  27633  noinfbnd2lem1  27648  noetasuplem4  27654  noetainflem4  27658  isinag  28771  axlowdimlem6  28880  axlowdimlem14  28888  pthdadjvtx  29664  uhgrwkspthlem2  29690  usgr2wlkspth  29695  usgr2trlncl  29696  pthdlem1  29702  lfgrn1cycl  29741  2wlkdlem5  29865  2pthdlem1  29866  3wlkdlem5  30098  3pthdlem1  30099  numclwwlkovh0  30307  numclwwlk2lem1  30311  numclwlk2lem2f  30312  numclwlk2lem2f1o  30314  eulplig  30420  opprqusdrng  33470  signsvvfval  34575  signsvfn  34579  bnj1534  34849  bnj1542  34853  bnj1280  35016  derangsn  35157  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  subfacp1  35173  fvtransport  36015  irrdiff  37309  poimirlem1  37610  poimirlem6  37615  poimirlem7  37616  cdlemkid3N  40922  cdlemkid4  40923  aks6d1c2p2  42102  hashscontpow  42105  sticksstones1  42129  sticksstones2  42130  stoweidlem43  46034  modm1nem2  47360  ichnreuop  47463  upgrimpthslem2  47898  isubgr3stgrlem4  47958  gpg5nbgrvtx13starlem2  48053  gpgprismgr4cycllem7  48081  pgnbgreunbgrlem1  48093  pgnbgreunbgrlem4  48099  pgnbgreunbgrlem5  48103  nnsgrpnmnd  48156  2zrngnmlid  48233  pgrpgt2nabl  48344  ldepsnlinc  48487