Theorem neeq12d 2993

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  2nreu  4384  fnelnfp  7132  2f1fvneq  7215  resf1extb  7885  suppval  8112  infpssrlem4  10228  injresinjlem  13745  sgrp2nmndlem5  18900  pmtr3ncom  19450  isnzr  20491  nzrpropd  20497  ptcmplem2  24018  ltsval2  27620  ltsres  27626  noseponlem  27628  noextenddif  27632  nosepnelem  27643  nosepeq  27649  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  isinag  28906  axlowdimlem6  29016  axlowdimlem14  29024  pthdadjvtx  29796  uhgrwkspthlem2  29822  usgr2wlkspth  29827  usgr2trlncl  29828  pthdlem1  29834  lfgrn1cycl  29873  2wlkdlem5  29997  2pthdlem1  29998  3wlkdlem5  30233  3pthdlem1  30234  numclwwlkovh0  30442  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  eulplig  30556  opprqusdrng  33553  signsvvfval  34722  signsvfn  34726  bnj1534  34995  bnj1542  34999  bnj1280  35162  derangsn  35352  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  subfacp1  35368  fvtransport  36214  mh-inf3f1  36723  irrdiff  37640  poimirlem1  37942  poimirlem6  37947  poimirlem7  37948  cdlemkid3N  41379  cdlemkid4  41380  aks6d1c2p2  42558  hashscontpow  42561  sticksstones1  42585  sticksstones2  42586  stoweidlem43  46471  modm1nem2  47823  ichnreuop  47932  upgrimpthslem2  48384  isubgr3stgrlem4  48445  gpg5nbgrvtx13starlem2  48548  gpgprismgr4cycllem7  48577  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  nnsgrpnmnd  48654  2zrngnmlid  48731  pgrpgt2nabl  48842  ldepsnlinc  48984