Theorem neeq12d 2987

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  2nreu  4410  fnelnfp  7154  2f1fvneq  7238  resf1extb  7913  suppval  8144  infpssrlem4  10266  injresinjlem  13755  sgrp2nmndlem5  18863  pmtr3ncom  19412  isnzr  20430  nzrpropd  20436  ptcmplem2  23947  sltval2  27575  sltres  27581  noseponlem  27583  noextenddif  27587  nosepnelem  27598  nosepeq  27604  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  isinag  28772  axlowdimlem6  28881  axlowdimlem14  28889  pthdadjvtx  29665  uhgrwkspthlem2  29691  usgr2wlkspth  29696  usgr2trlncl  29697  pthdlem1  29703  lfgrn1cycl  29742  2wlkdlem5  29866  2pthdlem1  29867  3wlkdlem5  30099  3pthdlem1  30100  numclwwlkovh0  30308  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  eulplig  30421  opprqusdrng  33471  signsvvfval  34576  signsvfn  34580  bnj1534  34850  bnj1542  34854  bnj1280  35017  derangsn  35164  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  subfacp1  35180  fvtransport  36027  irrdiff  37321  poimirlem1  37622  poimirlem6  37627  poimirlem7  37628  cdlemkid3N  40934  cdlemkid4  40935  aks6d1c2p2  42114  hashscontpow  42117  sticksstones1  42141  sticksstones2  42142  stoweidlem43  46048  modm1nem2  47374  ichnreuop  47477  upgrimpthslem2  47912  isubgr3stgrlem4  47972  gpg5nbgrvtx13starlem2  48067  gpgprismgr4cycllem7  48095  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  nnsgrpnmnd  48170  2zrngnmlid  48247  pgrpgt2nabl  48358  ldepsnlinc  48501