Theorem ifhvhv0 29285

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 29266	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4525	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 2108  ifcif 4456   ℋchba 29182  0_ℎc0v 29187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-hv0cl 29266

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  hvsubsub4  29323  hvnegdi  29330  hvsubeq0  29331  hvaddcan  29333  hvsubadd  29340  normlem9at  29384  normsq  29397  normsub0  29399  norm-ii  29401  norm-iii  29403  normsub  29406  normpyth  29408  norm3dif  29413  norm3lemt  29415  norm3adifi  29416  normpar  29418  polid  29422  bcs  29444  pjoc1  29697  pjoc2  29702  h1de2ci  29819  spansn  29822  elspansn  29829  elspansn2  29830  h1datom  29845  spansnj  29910  spansncv  29916  pjch1  29933  pjadji  29948  pjaddi  29949  pjinormi  29950  pjsubi  29951  pjmuli  29952  pjcjt2  29955  pjch  29957  pjopyth  29983  pjnorm  29987  pjpyth  29988  pjnel  29989  eigre  30098  eigorth  30101  lnopeq0lem2  30269  lnopunii  30275  lnophmi  30281  pjss2coi  30427  pjssmi  30428  pjssge0i  30429  pjdifnormi  30430