![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimivv | Unicode version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
exlimivv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | exlimiv 1598 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exlimiv 1598 |
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-gen 1449 ax-ie2 1494 ax-17 1526 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: cgsex2g 2773 cgsex4g 2774 opabss 4067 copsexg 4244 elopab 4258 epelg 4290 0nelelxp 4655 elvvuni 4690 optocl 4702 xpsspw 4738 relopabi 4752 relop 4777 elreldm 4853 xpmlem 5049 dfco2a 5129 unielrel 5156 oprabid 5906 1stval2 6155 2ndval2 6156 xp1st 6165 xp2nd 6166 poxp 6232 rntpos 6257 dftpos4 6263 tpostpos 6264 tfrlem7 6317 th3qlem2 6637 ener 6778 domtr 6784 unen 6815 xpsnen 6820 mapen 6845 ltdcnq 7395 archnqq 7415 enq0tr 7432 nqnq0pi 7436 nqnq0 7439 nqpnq0nq 7451 nqnq0a 7452 nqnq0m 7453 nq0m0r 7454 nq0a0 7455 nq02m 7463 prarloc 7501 axaddcl 7862 axmulcl 7864 hashfacen 10811 bj-inex 14541 |
Copyright terms: Public domain | W3C validator |