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 1489 | . 2 |
3 | 2 | exlimiv 1489 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-gen 1338 ax-ie2 1383 ax-17 1419 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: cgsex2g 2590 cgsex4g 2591 opabss 3821 copsexg 3981 elopab 3995 epelg 4027 0nelelxp 4373 elvvuni 4404 optocl 4416 xpsspw 4450 relopabi 4463 relop 4486 elreldm 4560 xpmlem 4744 dfco2a 4821 unielrel 4845 oprabid 5537 1stval2 5782 2ndval2 5783 xp1st 5792 xp2nd 5793 poxp 5853 rntpos 5872 dftpos4 5878 tpostpos 5879 tfrlem7 5933 th3qlem2 6209 ener 6259 domtr 6265 unen 6293 xpsnen 6295 ltdcnq 6495 archnqq 6515 enq0tr 6532 nqnq0pi 6536 nqnq0 6539 nqpnq0nq 6551 nqnq0a 6552 nqnq0m 6553 nq0m0r 6554 nq0a0 6555 nq02m 6563 prarloc 6601 axaddcl 6940 axmulcl 6942 bj-inex 10027 |
Copyright terms: Public domain | W3C validator |