Theorem neeq12d 3020

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 3003	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960

This theorem is used by:  2nreu  4405  fnelnfp  7205  2f1fvneq  7287  resf1extb  7970  suppval  8206  infpssrlem4  10411  injresinjlem  13952  sgrp2nmndlem5  19157  pmtr3ncom  19719  isnzr  20794  nzrpropd  20801  ptcmplem2  24402  fltoprm  28025  fltoprmgt3  28026  ltsval2  28043  ltsres  28049  noseponlem  28051  noextenddif  28055  nosepnelem  28066  nosepeq  28072  nosupbnd2lem1  28102  noinfbnd2lem1  28117  noetasuplem4  28123  noetainflem4  28127  isinag  29387  elcgrabasi  29405  elcgrabasrd  29406  cgrabasimass  29408  axlowdimlem6  29555  axlowdimlem14  29563  pthdadjvtx  30343  uhgrwkspthlem2  30370  usgr2wlkspth  30375  usgr2trlncl  30376  pthdlem1  30382  lfgrn1cycl  30424  2wlkdlem5  30548  2pthdlem1  30549  3wlkdlem5  30794  3pthdlem1  30795  numclwwlkovh0  31003  numclwwlk2lem1  31007  numclwlk2lem2f  31008  numclwlk2lem2f1o  31010  eulplig  31117  opprqusdrng  34087  signsvvfval  35277  signsvfn  35281  bnj1534  35553  bnj1542  35557  bnj1280  35720  derangsn  36102  derangenlem  36103  subfacp1lem3  36114  subfacp1lem5  36116  subfacp1lem6  36117  subfacp1  36118  fvtransport  36975  irrdiff  38439  poimirlem1  38731  poimirlem6  38736  poimirlem7  38737  cdlemkid3N  42182  cdlemkid4  42183  aks6d1c2p2  43361  hashscontpow  43364  sticksstones1  43388  sticksstones2  43389  stoweidlem43  47258  modm1nem2  48650  ichnreuop  48759  upgrimpthslem2  49211  isubgr3stgrlem4  49272  gpg5nbgrvtx13starlem2  49375  gpgprismgr4cycllem7  49404  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem4  49422  pgnbgreunbgrlem5  49426  nnsgrpnmnd  49480  2zrngnmlid  49557  pgrpgt2nabl  49683  ldepsnlinc  49825