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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  2nreu  4402  fnelnfp  7174  2f1fvneq  7256  resf1extb  7935  suppval  8163  infpssrlem4  10365  injresinjlem  13905  sgrp2nmndlem5  19108  pmtr3ncom  19669  isnzr  20744  nzrpropd  20751  ptcmplem2  24352  fltoprm  27977  fltoprmgt3  27978  ltsval2  27995  ltsres  28001  noseponlem  28003  noextenddif  28007  nosepnelem  28018  nosepeq  28024  nosupbnd2lem1  28054  noinfbnd2lem1  28069  noetasuplem4  28075  noetainflem4  28079  isinag  29339  elcgrabasi  29357  elcgrabasrd  29358  cgrabasimass  29360  axlowdimlem6  29507  axlowdimlem14  29515  pthdadjvtx  30295  uhgrwkspthlem2  30322  usgr2wlkspth  30327  usgr2trlncl  30328  pthdlem1  30334  lfgrn1cycl  30376  2wlkdlem5  30500  2pthdlem1  30501  3wlkdlem5  30746  3pthdlem1  30747  numclwwlkovh0  30955  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  eulplig  31069  opprqusdrng  33999  signsvvfval  35190  signsvfn  35194  bnj1534  35466  bnj1542  35470  bnj1280  35633  derangsn  35904  derangenlem  35905  subfacp1lem3  35916  subfacp1lem5  35918  subfacp1lem6  35919  subfacp1  35920  fvtransport  36767  irrdiff  38215  poimirlem1  38507  poimirlem6  38512  poimirlem7  38513  cdlemkid3N  41958  cdlemkid4  41959  aks6d1c2p2  43137  hashscontpow  43140  sticksstones1  43164  sticksstones2  43165  stoweidlem43  46997  modm1nem2  48389  ichnreuop  48498  upgrimpthslem2  48950  isubgr3stgrlem4  49011  gpg5nbgrvtx13starlem2  49114  gpgprismgr4cycllem7  49143  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5  49165  nnsgrpnmnd  49219  2zrngnmlid  49296  pgrpgt2nabl  49422  ldepsnlinc  49564