Theorem neeq12d 2999

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  2nreu  4449  fnelnfp  7196  suppval  8185  infpssrlem4  10343  injresinjlem  13822  sgrp2nmndlem5  18954  pmtr3ncom  19507  isnzr  20530  nzrpropd  20536  ptcmplem2  24076  sltval2  27715  sltres  27721  noseponlem  27723  noextenddif  27727  nosepnelem  27738  nosepeq  27744  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  isinag  28860  axlowdimlem6  28976  axlowdimlem14  28984  pthdadjvtx  29762  uhgrwkspthlem2  29786  usgr2wlkspth  29791  usgr2trlncl  29792  pthdlem1  29798  lfgrn1cycl  29834  2wlkdlem5  29958  2pthdlem1  29959  3wlkdlem5  30191  3pthdlem1  30192  numclwwlkovh0  30400  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  eulplig  30513  opprqusdrng  33500  signsvvfval  34571  signsvfn  34575  bnj1534  34845  bnj1542  34849  bnj1280  35012  derangsn  35154  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  subfacp1lem6  35169  subfacp1  35170  fvtransport  36013  irrdiff  37308  poimirlem1  37607  poimirlem6  37612  poimirlem7  37613  cdlemkid3N  40915  cdlemkid4  40916  aks6d1c2p2  42100  hashscontpow  42103  sticksstones1  42127  sticksstones2  42128  stoweidlem43  45998  ichnreuop  47396  isubgr3stgrlem4  47871  gpg5nbgrvtx13starlem2  47962  nnsgrpnmnd  48021  2zrngnmlid  48098  pgrpgt2nabl  48210  ldepsnlinc  48353