Theorem neeq12d 3021

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  2nreu  4401  fnelnfp  7165  2f1fvneq  7248  resf1extb  7919  suppval  8146  infpssrlem4  10278  injresinjlem  13810  sgrp2nmndlem5  18981  pmtr3ncom  19536  isnzr  20588  nzrpropd  20595  ptcmplem2  24171  ltsval2  27778  ltsres  27784  noseponlem  27786  noextenddif  27790  nosepnelem  27801  nosepeq  27807  nosupbnd2lem1  27837  noinfbnd2lem1  27852  noetasuplem4  27858  noetainflem4  27862  isinag  29090  axlowdimlem6  29206  axlowdimlem14  29214  pthdadjvtx  29986  uhgrwkspthlem2  30012  usgr2wlkspth  30017  usgr2trlncl  30018  pthdlem1  30024  lfgrn1cycl  30063  2wlkdlem5  30187  2pthdlem1  30188  3wlkdlem5  30423  3pthdlem1  30424  numclwwlkovh0  30632  numclwwlk2lem1  30636  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  eulplig  30746  opprqusdrng  33692  signsvvfval  34882  signsvfn  34886  bnj1534  35158  bnj1542  35162  bnj1280  35325  derangsn  35533  derangenlem  35534  subfacp1lem3  35545  subfacp1lem5  35547  subfacp1lem6  35548  subfacp1  35549  fvtransport  36395  mh-inf3f1  36914  irrdiff  37830  poimirlem1  38132  poimirlem6  38137  poimirlem7  38138  cdlemkid3N  41569  cdlemkid4  41570  aks6d1c2p2  42748  hashscontpow  42751  sticksstones1  42775  sticksstones2  42776  stoweidlem43  46615  modm1nem2  47967  ichnreuop  48076  upgrimpthslem2  48528  isubgr3stgrlem4  48589  gpg5nbgrvtx13starlem2  48692  gpgprismgr4cycllem7  48721  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem4  48739  pgnbgreunbgrlem5  48743  nnsgrpnmnd  48798  2zrngnmlid  48875  pgrpgt2nabl  48997  ldepsnlinc  49139