Theorem nelprd 4609

Description: If an element doesn't match the items in an unordered pair, it is not in the unordered pair, deduction version. (Contributed by Alexander van der Vekens, 25-Jan-2018.)

Hypotheses

Ref	Expression
nelprd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)
nelprd.2	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Assertion

Ref	Expression
nelprd	⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})

Proof of Theorem nelprd

Step	Hyp	Ref	Expression
1		nelprd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		nelprd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
3		neanior 3018	. . 3 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
4		elpri 4601	. . . 4 ⊢ (𝐴 ∈ {𝐵, 𝐶} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶))
5	4	con3i 154	. . 3 ⊢ (¬ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
6	3, 5	sylbi 217	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ¬ 𝐴 ∈ {𝐵, 𝐶})
7	1, 2, 6	syl2anc 584	1 ⊢ (𝜑 → ¬ 𝐴 ∈ {𝐵, 𝐶})

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  {cpr 4579

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-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580

This theorem is referenced by:  ord2eln012  8415  renfdisj  11175  sumtp  15656  pmtrprfv3  19333  logbgcd1irr  26702  perfectlem2  27139  nbupgrres  29309  usgr2pthlem  29708  eupth2lem3lem6  30177  cycpmco2  33076  cyc2fvx  33077  elrspunsn  33367  relogbzexpd  41958  dvrelog2b  42049  dvrelogpow2b  42051  aks4d1p1p4  42054  aks4d1p6  42064  aks6d1c7lem1  42163  mnuprdlem1  44255  mnuprdlem2  44256  perfectALTVlem2  47716