![]() |
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 1558 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | exlimiv 1558 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-gen 1406 ax-ie2 1451 ax-17 1487 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: cgsex2g 2691 cgsex4g 2692 opabss 3950 copsexg 4124 elopab 4138 epelg 4170 0nelelxp 4526 elvvuni 4561 optocl 4573 xpsspw 4609 relopabi 4623 relop 4647 elreldm 4723 xpmlem 4915 dfco2a 4995 unielrel 5022 oprabid 5755 1stval2 6005 2ndval2 6006 xp1st 6015 xp2nd 6016 poxp 6081 rntpos 6106 dftpos4 6112 tpostpos 6113 tfrlem7 6166 th3qlem2 6484 ener 6625 domtr 6631 unen 6662 xpsnen 6666 mapen 6691 ltdcnq 7147 archnqq 7167 enq0tr 7184 nqnq0pi 7188 nqnq0 7191 nqpnq0nq 7203 nqnq0a 7204 nqnq0m 7205 nq0m0r 7206 nq0a0 7207 nq02m 7215 prarloc 7253 axaddcl 7593 axmulcl 7595 hashfacen 10466 bj-inex 12788 |
Copyright terms: Public domain | W3C validator |