Theorem ifhvhv0 27263

Description: Prove if(𝐴 ∈ ℋ, 𝐴, 0_ℎ) ∈ ℋ (common case). (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 27244	. 2 ⊢ 0ℎ ∈ ℋ
2	1	elimel 4100	1 ⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ

Syntax hints:   ∈ wcel 1977  ifcif 4036   ℋchil 27160  0_ℎc0v 27165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-hv0cl 27244

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  hvsubsub4  27301  hvnegdi  27308  hvsubeq0  27309  hvaddcan  27311  hvsubadd  27318  normlem9at  27362  normsq  27375  normsub0  27377  norm-ii  27379  norm-iii  27381  normsub  27384  normpyth  27386  norm3dif  27391  norm3lemt  27393  norm3adifi  27394  normpar  27396  polid  27400  bcs  27422  pjoc1  27677  pjoc2  27682  h1de2ci  27799  spansn  27802  elspansn  27809  elspansn2  27810  h1datom  27825  spansnj  27890  spansncv  27896  pjch1  27913  pjadji  27928  pjaddi  27929  pjinormi  27930  pjsubi  27931  pjmuli  27932  pjcjt2  27935  pjch  27937  pjopyth  27963  pjnorm  27967  pjpyth  27968  pjnel  27969  eigre  28078  eigorth  28081  lnopeq0lem2  28249  lnopunii  28255  lnophmi  28261  pjss2coi  28407  pjssmi  28408  pjssge0i  28409  pjdifnormi  28410