Theorem neeq12d 2989

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  2nreu  4394  fnelnfp  7111  2f1fvneq  7194  resf1extb  7864  suppval  8092  infpssrlem4  10194  injresinjlem  13687  sgrp2nmndlem5  18834  pmtr3ncom  19385  isnzr  20427  nzrpropd  20433  ptcmplem2  23966  sltval2  27593  sltres  27599  noseponlem  27601  noextenddif  27605  nosepnelem  27616  nosepeq  27622  nosupbnd2lem1  27652  noinfbnd2lem1  27667  noetasuplem4  27673  noetainflem4  27677  isinag  28814  axlowdimlem6  28923  axlowdimlem14  28931  pthdadjvtx  29704  uhgrwkspthlem2  29730  usgr2wlkspth  29735  usgr2trlncl  29736  pthdlem1  29742  lfgrn1cycl  29781  2wlkdlem5  29905  2pthdlem1  29906  3wlkdlem5  30138  3pthdlem1  30139  numclwwlkovh0  30347  numclwwlk2lem1  30351  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  eulplig  30460  opprqusdrng  33453  signsvvfval  34586  signsvfn  34590  bnj1534  34860  bnj1542  34864  bnj1280  35027  derangsn  35202  derangenlem  35203  subfacp1lem3  35214  subfacp1lem5  35216  subfacp1lem6  35217  subfacp1  35218  fvtransport  36065  irrdiff  37359  poimirlem1  37660  poimirlem6  37665  poimirlem7  37666  cdlemkid3N  40971  cdlemkid4  40972  aks6d1c2p2  42151  hashscontpow  42154  sticksstones1  42178  sticksstones2  42179  stoweidlem43  46080  modm1nem2  47399  ichnreuop  47502  upgrimpthslem2  47938  isubgr3stgrlem4  47999  gpg5nbgrvtx13starlem2  48102  gpgprismgr4cycllem7  48131  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem4  48149  pgnbgreunbgrlem5  48153  nnsgrpnmnd  48208  2zrngnmlid  48285  pgrpgt2nabl  48396  ldepsnlinc  48539