![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elv | GIF version |
Description: Technical lemma used to shorten proofs. If a proposition is implied by 𝑥 ∈ V (which is true, see vex 2740), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.) |
Ref | Expression |
---|---|
elv.1 | ⊢ (𝑥 ∈ V → 𝜑) |
Ref | Expression |
---|---|
elv | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2740 | . 2 ⊢ 𝑥 ∈ V | |
2 | elv.1 | . 2 ⊢ (𝑥 ∈ V → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 Vcvv 2737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-v 2739 |
This theorem is referenced by: xpiindim 4764 disjxp1 6236 ixpiinm 6723 ixpsnf1o 6735 iunfidisj 6944 ssfii 6972 fifo 6978 dcfi 6979 omp1eomlem 7092 exmidomniim 7138 bcval5 10738 rexfiuz 10993 fsum2dlemstep 11437 fsumcnv 11440 fisumcom2 11441 fsumconst 11457 modfsummodlemstep 11460 fsumabs 11468 fprodcllemf 11616 fprod2dlemstep 11625 fprodcnv 11628 fprodcom2fi 11629 fprodmodd 11644 ennnfonelemim 12419 topnfn 12683 ismgm 12730 issgrp 12763 ismnddef 12773 isnsg 13015 fnmgp 13085 isring 13136 iuncld 13508 txbas 13651 txdis 13670 xmetunirn 13751 xmettxlem 13902 xmettx 13903 pw1nct 14634 |
Copyright terms: Public domain | W3C validator |