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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  2nreu  4419  fnelnfp  7169  2f1fvneq  7253  resf1extb  7930  suppval  8161  infpssrlem4  10320  injresinjlem  13803  sgrp2nmndlem5  18907  pmtr3ncom  19456  isnzr  20474  nzrpropd  20480  ptcmplem2  23991  sltval2  27620  sltres  27626  noseponlem  27628  noextenddif  27632  nosepnelem  27643  nosepeq  27649  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  isinag  28817  axlowdimlem6  28926  axlowdimlem14  28934  pthdadjvtx  29710  uhgrwkspthlem2  29736  usgr2wlkspth  29741  usgr2trlncl  29742  pthdlem1  29748  lfgrn1cycl  29787  2wlkdlem5  29911  2pthdlem1  29912  3wlkdlem5  30144  3pthdlem1  30145  numclwwlkovh0  30353  numclwwlk2lem1  30357  numclwlk2lem2f  30358  numclwlk2lem2f1o  30360  eulplig  30466  opprqusdrng  33508  signsvvfval  34610  signsvfn  34614  bnj1534  34884  bnj1542  34888  bnj1280  35051  derangsn  35192  derangenlem  35193  subfacp1lem3  35204  subfacp1lem5  35206  subfacp1lem6  35207  subfacp1  35208  fvtransport  36050  irrdiff  37344  poimirlem1  37645  poimirlem6  37650  poimirlem7  37651  cdlemkid3N  40952  cdlemkid4  40953  aks6d1c2p2  42132  hashscontpow  42135  sticksstones1  42159  sticksstones2  42160  stoweidlem43  46072  ichnreuop  47486  upgrimpthslem2  47921  isubgr3stgrlem4  47981  gpg5nbgrvtx13starlem2  48074  gpgprismgr4cycllem7  48100  nnsgrpnmnd  48153  2zrngnmlid  48230  pgrpgt2nabl  48341  ldepsnlinc  48484