Theorem neeq12d 2986

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

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

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 2701

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

This theorem is referenced by:  2nreu  4407  fnelnfp  7151  2f1fvneq  7235  resf1extb  7910  suppval  8141  infpssrlem4  10259  injresinjlem  13748  sgrp2nmndlem5  18856  pmtr3ncom  19405  isnzr  20423  nzrpropd  20429  ptcmplem2  23940  sltval2  27568  sltres  27574  noseponlem  27576  noextenddif  27580  nosepnelem  27591  nosepeq  27597  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  isinag  28765  axlowdimlem6  28874  axlowdimlem14  28882  pthdadjvtx  29658  uhgrwkspthlem2  29684  usgr2wlkspth  29689  usgr2trlncl  29690  pthdlem1  29696  lfgrn1cycl  29735  2wlkdlem5  29859  2pthdlem1  29860  3wlkdlem5  30092  3pthdlem1  30093  numclwwlkovh0  30301  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  eulplig  30414  opprqusdrng  33464  signsvvfval  34569  signsvfn  34573  bnj1534  34843  bnj1542  34847  bnj1280  35010  derangsn  35157  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  subfacp1  35173  fvtransport  36020  irrdiff  37314  poimirlem1  37615  poimirlem6  37620  poimirlem7  37621  cdlemkid3N  40927  cdlemkid4  40928  aks6d1c2p2  42107  hashscontpow  42110  sticksstones1  42134  sticksstones2  42135  stoweidlem43  46041  modm1nem2  47370  ichnreuop  47473  upgrimpthslem2  47908  isubgr3stgrlem4  47968  gpg5nbgrvtx13starlem2  48063  gpgprismgr4cycllem7  48091  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  nnsgrpnmnd  48166  2zrngnmlid  48243  pgrpgt2nabl  48354  ldepsnlinc  48497