Theorem neeq12d 3017

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  2nreu  4397  fnelnfp  7157  2f1fvneq  7240  resf1extb  7911  suppval  8137  infpssrlem4  10260  injresinjlem  13793  sgrp2nmndlem5  18949  pmtr3ncom  19498  isnzr  20543  nzrpropd  20549  ptcmplem2  24093  ltsval2  27697  ltsres  27703  noseponlem  27705  noextenddif  27709  nosepnelem  27720  nosepeq  27726  nosupbnd2lem1  27756  noinfbnd2lem1  27771  noetasuplem4  27777  noetainflem4  27781  isinag  28984  axlowdimlem6  29094  axlowdimlem14  29102  pthdadjvtx  29874  uhgrwkspthlem2  29900  usgr2wlkspth  29905  usgr2trlncl  29906  pthdlem1  29912  lfgrn1cycl  29951  2wlkdlem5  30075  2pthdlem1  30076  3wlkdlem5  30311  3pthdlem1  30312  numclwwlkovh0  30520  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  eulplig  30634  opprqusdrng  33642  signsvvfval  34836  signsvfn  34840  bnj1534  35112  bnj1542  35116  bnj1280  35279  derangsn  35484  derangenlem  35485  subfacp1lem3  35496  subfacp1lem5  35498  subfacp1lem6  35499  subfacp1  35500  fvtransport  36346  mh-inf3f1  36865  irrdiff  37782  poimirlem1  38084  poimirlem6  38089  poimirlem7  38090  cdlemkid3N  41521  cdlemkid4  41522  aks6d1c2p2  42700  hashscontpow  42703  sticksstones1  42727  sticksstones2  42728  stoweidlem43  46581  modm1nem2  47933  ichnreuop  48042  upgrimpthslem2  48494  isubgr3stgrlem4  48555  gpg5nbgrvtx13starlem2  48658  gpgprismgr4cycllem7  48687  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem4  48705  pgnbgreunbgrlem5  48709  nnsgrpnmnd  48764  2zrngnmlid  48841  pgrpgt2nabl  48952  ldepsnlinc  49094