![]() |
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 2740 |
. 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 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 4759 disjxp1 6230 ixpiinm 6717 ixpsnf1o 6729 iunfidisj 6938 ssfii 6966 fifo 6972 dcfi 6973 omp1eomlem 7086 exmidomniim 7132 bcval5 10714 rexfiuz 10969 fsum2dlemstep 11413 fsumcnv 11416 fisumcom2 11417 fsumconst 11433 modfsummodlemstep 11436 fsumabs 11444 fprodcllemf 11592 fprod2dlemstep 11601 fprodcnv 11604 fprodcom2fi 11605 fprodmodd 11620 ennnfonelemim 12395 topnfn 12628 ismgm 12655 issgrp 12688 ismnddef 12698 fnmgp 12946 isring 12996 iuncld 13248 txbas 13391 txdis 13410 xmetunirn 13491 xmettxlem 13642 xmettx 13643 pw1nct 14375 |
Copyright terms: Public domain | W3C validator |