Theorem neeq12d 3018

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

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

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 2734

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

This theorem is used by:  2nreu  4405  fnelnfp  7179  2f1fvneq  7261  resf1extb  7935  suppval  8164  infpssrlem4  10312  injresinjlem  13850  sgrp2nmndlem5  19047  pmtr3ncom  19608  isnzr  20680  nzrpropd  20687  ptcmplem2  24285  ltsval2  27900  ltsres  27906  noseponlem  27908  noextenddif  27912  nosepnelem  27923  nosepeq  27929  nosupbnd2lem1  27959  noinfbnd2lem1  27974  noetasuplem4  27980  noetainflem4  27984  isinag  29244  elcgrabasi  29262  elcgrabasrd  29263  cgrabasimass  29265  axlowdimlem6  29412  axlowdimlem14  29420  pthdadjvtx  30200  uhgrwkspthlem2  30227  usgr2wlkspth  30232  usgr2trlncl  30233  pthdlem1  30239  lfgrn1cycl  30281  2wlkdlem5  30405  2pthdlem1  30406  3wlkdlem5  30651  3pthdlem1  30652  numclwwlkovh0  30860  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  eulplig  30974  opprqusdrng  33903  signsvvfval  35094  signsvfn  35098  bnj1534  35370  bnj1542  35374  bnj1280  35537  derangsn  35757  derangenlem  35758  subfacp1lem3  35769  subfacp1lem5  35771  subfacp1lem6  35772  subfacp1  35773  fvtransport  36620  mh-inf3f1  37168  irrdiff  38086  poimirlem1  38378  poimirlem6  38383  poimirlem7  38384  cdlemkid3N  41814  cdlemkid4  41815  aks6d1c2p2  42993  hashscontpow  42996  sticksstones1  43020  sticksstones2  43021  stoweidlem43  46879  modm1nem2  48271  ichnreuop  48380  upgrimpthslem2  48832  isubgr3stgrlem4  48893  gpg5nbgrvtx13starlem2  48996  gpgprismgr4cycllem7  49025  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5  49047  nnsgrpnmnd  49101  2zrngnmlid  49178  pgrpgt2nabl  49304  ldepsnlinc  49446