Theorem ifhvhv0 31558

Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0_ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)

Assertion

Ref	Expression
ifhvhv0	⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Proof of Theorem ifhvhv0

Step	Hyp	Ref	Expression
1		ax-hv0cl 31539	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4551	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

This proof depends on syntax axioms:   ∈ wcel 2145  ifcif 4481   ℋchba 31455  0_ℎc0v 31460

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-hv0cl 31539

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  hvsubsub4  31596  hvnegdi  31603  hvsubeq0  31604  hvaddcan  31606  hvsubadd  31613  normlem9at  31657  normsq  31670  normsub0  31672  norm-ii  31674  norm-iii  31676  normsub  31679  normpyth  31681  norm3dif  31686  norm3lemt  31688  norm3adifi  31689  normpar  31691  polid  31695  bcs  31717  pjoc1  31970  pjoc2  31975  h1de2ci  32092  spansn  32095  elspansn  32102  elspansn2  32103  h1datom  32118  spansnj  32183  spansncv  32189  pjch1  32206  pjadji  32221  pjaddi  32222  pjinormi  32223  pjsubi  32224  pjmuli  32225  pjcjt2  32228  pjch  32230  pjopyth  32256  pjnorm  32260  pjpyth  32261  pjnel  32262  eigre  32371  eigorth  32374  lnopeq0lem2  32542  lnopunii  32548  lnophmi  32554  pjss2coi  32700  pjssmi  32701  pjssge0i  32702  pjdifnormi  32703