![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elv | Unicode version |
Description: Technical lemma used to
shorten proofs. If a proposition is implied by
![]() ![]() ![]() |
Ref | Expression |
---|---|
elv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elv |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2755 |
. 2
![]() ![]() ![]() ![]() | |
2 | elv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-v 2754 |
This theorem is referenced by: xpiindim 4782 disjxp1 6261 ixpiinm 6750 ixpsnf1o 6762 iunfidisj 6975 ssfii 7003 fifo 7009 dcfi 7010 omp1eomlem 7123 exmidomniim 7169 bcval5 10775 rexfiuz 11030 fsum2dlemstep 11474 fsumcnv 11477 fisumcom2 11478 fsumconst 11494 modfsummodlemstep 11497 fsumabs 11505 fprodcllemf 11653 fprod2dlemstep 11662 fprodcnv 11665 fprodcom2fi 11666 fprodmodd 11681 4sqleminfi 12429 ennnfonelemim 12475 topnfn 12749 ptex 12769 xpsff1o 12825 ismgm 12833 issgrp 12866 ismnddef 12879 isnsg 13141 fnmgp 13276 isrng 13288 isring 13354 dfrhm2 13504 znval 13932 iuncld 14075 txbas 14218 txdis 14237 xmetunirn 14318 xmettxlem 14469 xmettx 14470 pw1nct 15214 |
Copyright terms: Public domain | W3C validator |