Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > ifhvhv0 | Structured version Visualization version Unicode version |
Description: Prove (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ifhvhv0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hv0cl 27860 | . 2 | |
2 | 1 | elimel 4150 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 cif 4086 chil 27776 c0v 27781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-hv0cl 27860 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-if 4087 |
This theorem is referenced by: hvsubsub4 27917 hvnegdi 27924 hvsubeq0 27925 hvaddcan 27927 hvsubadd 27934 normlem9at 27978 normsq 27991 normsub0 27993 norm-ii 27995 norm-iii 27997 normsub 28000 normpyth 28002 norm3dif 28007 norm3lemt 28009 norm3adifi 28010 normpar 28012 polid 28016 bcs 28038 pjoc1 28293 pjoc2 28298 h1de2ci 28415 spansn 28418 elspansn 28425 elspansn2 28426 h1datom 28441 spansnj 28506 spansncv 28512 pjch1 28529 pjadji 28544 pjaddi 28545 pjinormi 28546 pjsubi 28547 pjmuli 28548 pjcjt2 28551 pjch 28553 pjopyth 28579 pjnorm 28583 pjpyth 28584 pjnel 28585 eigre 28694 eigorth 28697 lnopeq0lem2 28865 lnopunii 28871 lnophmi 28877 pjss2coi 29023 pjssmi 29024 pjssge0i 29025 pjdifnormi 29026 |
Copyright terms: Public domain | W3C validator |