Theorem tpid3 4717

Description: One of the three elements of an unordered triple. (Contributed by NM, 7-Apr-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 30-Apr-2021.)

Hypothesis

Ref	Expression
tpid3.1	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
tpid3	⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Proof of Theorem tpid3

Step	Hyp	Ref	Expression
1		tpid3.1	. 2 ⊢ 𝐶 ∈ V
2		tpid3g 4716	. 2 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐴, 𝐵, 𝐶})
3	1, 2	ax-mp 5	1 ⊢ 𝐶 ∈ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {ctp 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570  df-tp 4572

This theorem is referenced by:  hash3tpb  14457  wrdl3s3  14924  usgrwwlks2on  30026  umgrwwlks2on  30027  ex-pss  30498  sgncl  32904  s3rnOLD  33006  cyc3evpm  33211  sgnsf  33223  prodfzo03  34747  circlevma  34786  circlemethhgt  34787  hgt750lemg  34798  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  kur14lem7  35394  brtpid3  35905  rabren3dioph  43243  oenord1ex  43743  fourierdlem114  46648  usgrexmpl1tri  48501  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  gpg3kgrtriex  48565