Theorem neeq12d 3016

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  2nreu  4401  fnelnfp  7182  2f1fvneq  7264  resf1extb  7946  suppval  8181  infpssrlem4  10387  injresinjlem  13928  sgrp2nmndlem5  19133  pmtr3ncom  19694  isnzr  20769  nzrpropd  20776  ptcmplem2  24377  fltoprm  28000  fltoprmgt3  28001  ltsval2  28018  ltsres  28024  noseponlem  28026  noextenddif  28030  nosepnelem  28041  nosepeq  28047  nosupbnd2lem1  28077  noinfbnd2lem1  28092  noetasuplem4  28098  noetainflem4  28102  isinag  29362  elcgrabasi  29380  elcgrabasrd  29381  cgrabasimass  29383  axlowdimlem6  29530  axlowdimlem14  29538  pthdadjvtx  30318  uhgrwkspthlem2  30345  usgr2wlkspth  30350  usgr2trlncl  30351  pthdlem1  30357  lfgrn1cycl  30399  2wlkdlem5  30523  2pthdlem1  30524  3wlkdlem5  30769  3pthdlem1  30770  numclwwlkovh0  30978  numclwwlk2lem1  30982  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  eulplig  31092  opprqusdrng  34063  signsvvfval  35253  signsvfn  35257  bnj1534  35529  bnj1542  35533  bnj1280  35696  derangsn  36021  derangenlem  36022  subfacp1lem3  36033  subfacp1lem5  36035  subfacp1lem6  36036  subfacp1  36037  fvtransport  36889  irrdiff  38340  poimirlem1  38632  poimirlem6  38637  poimirlem7  38638  cdlemkid3N  42083  cdlemkid4  42084  aks6d1c2p2  43262  hashscontpow  43265  sticksstones1  43289  sticksstones2  43290  stoweidlem43  47146  modm1nem2  48538  ichnreuop  48647  upgrimpthslem2  49099  isubgr3stgrlem4  49160  gpg5nbgrvtx13starlem2  49263  gpgprismgr4cycllem7  49292  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem4  49310  pgnbgreunbgrlem5  49314  nnsgrpnmnd  49368  2zrngnmlid  49445  pgrpgt2nabl  49571  ldepsnlinc  49713