Theorem neeq12d 2990

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  2nreu  4393  fnelnfp  7117  2f1fvneq  7200  resf1extb  7870  suppval  8098  infpssrlem4  10204  injresinjlem  13692  sgrp2nmndlem5  18839  pmtr3ncom  19389  isnzr  20431  nzrpropd  20437  ptcmplem2  23969  sltval2  27596  sltres  27602  noseponlem  27604  noextenddif  27608  nosepnelem  27619  nosepeq  27625  nosupbnd2lem1  27655  noinfbnd2lem1  27670  noetasuplem4  27676  noetainflem4  27680  isinag  28817  axlowdimlem6  28927  axlowdimlem14  28935  pthdadjvtx  29708  uhgrwkspthlem2  29734  usgr2wlkspth  29739  usgr2trlncl  29740  pthdlem1  29746  lfgrn1cycl  29785  2wlkdlem5  29909  2pthdlem1  29910  3wlkdlem5  30145  3pthdlem1  30146  numclwwlkovh0  30354  numclwwlk2lem1  30358  numclwlk2lem2f  30359  numclwlk2lem2f1o  30361  eulplig  30467  opprqusdrng  33465  signsvvfval  34612  signsvfn  34616  bnj1534  34886  bnj1542  34890  bnj1280  35053  derangsn  35235  derangenlem  35236  subfacp1lem3  35247  subfacp1lem5  35249  subfacp1lem6  35250  subfacp1  35251  fvtransport  36097  irrdiff  37391  poimirlem1  37681  poimirlem6  37686  poimirlem7  37687  cdlemkid3N  41052  cdlemkid4  41053  aks6d1c2p2  42232  hashscontpow  42235  sticksstones1  42259  sticksstones2  42260  stoweidlem43  46165  modm1nem2  47493  ichnreuop  47596  upgrimpthslem2  48032  isubgr3stgrlem4  48093  gpg5nbgrvtx13starlem2  48196  gpgprismgr4cycllem7  48225  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem4  48243  pgnbgreunbgrlem5  48247  nnsgrpnmnd  48302  2zrngnmlid  48379  pgrpgt2nabl  48490  ldepsnlinc  48633