![]() |
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 10742 rexfiuz 10997 fsum2dlemstep 11441 fsumcnv 11444 fisumcom2 11445 fsumconst 11461 modfsummodlemstep 11464 fsumabs 11472 fprodcllemf 11620 fprod2dlemstep 11629 fprodcnv 11632 fprodcom2fi 11633 fprodmodd 11648 ennnfonelemim 12424 topnfn 12692 ptex 12712 xpsff1o 12767 ismgm 12775 issgrp 12808 ismnddef 12818 isnsg 13060 fnmgp 13130 isring 13181 iuncld 13585 txbas 13728 txdis 13747 xmetunirn 13828 xmettxlem 13979 xmettx 13980 pw1nct 14722 |
Copyright terms: Public domain | W3C validator |