Theorem eltpi 4627

Description: A member of an unordered triple of classes is one of them. (Contributed by Mario Carneiro, 11-Feb-2015.)

Assertion

Ref	Expression
eltpi	⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

Proof of Theorem eltpi

Step	Hyp	Ref	Expression
1		eltpg 4625	. 2 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 ∈ {𝐵, 𝐶, 𝐷} ↔ (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷)))
2	1	ibi 268	1 ⊢ (𝐴 ∈ {𝐵, 𝐶, 𝐷} → (𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ∨ 𝐴 = 𝐷))

Syntax hints:   → wi 4   ∨ w3o 1091   = wceq 1547   ∈ wcel 2119  {ctp 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565  df-tp 4567

This theorem is referenced by:  fvf1tp  13746  tpfo  14460  prm23lt5  16783  perfectlem2  27218  zabsle1  27284  sgnmulsgn  32941  sgnmulsgp  32942  gsumtp  33152  cyc3co2  33228  kur14lem7  35447  omcl3g  43786  fmtnofz04prm  48062  perfectALTVlem2  48220  gpgprismgr4cycllem7  48599  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem6  48622