![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimivv | GIF 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 1609 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1609 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1503 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-gen 1460 ax-ie2 1505 ax-17 1537 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: cgsex2g 2788 cgsex4g 2789 opabss 4082 copsexg 4262 elopab 4276 epelg 4308 0nelelxp 4673 elvvuni 4708 optocl 4720 xpsspw 4756 relopabi 4770 relop 4795 elreldm 4871 xpmlem 5067 dfco2a 5147 unielrel 5174 oprabid 5929 1stval2 6181 2ndval2 6182 xp1st 6191 xp2nd 6192 poxp 6258 rntpos 6283 dftpos4 6289 tpostpos 6290 tfrlem7 6343 th3qlem2 6665 ener 6806 domtr 6812 unen 6843 xpsnen 6848 mapen 6875 ltdcnq 7427 archnqq 7447 enq0tr 7464 nqnq0pi 7468 nqnq0 7471 nqpnq0nq 7483 nqnq0a 7484 nqnq0m 7485 nq0m0r 7486 nq0a0 7487 nq02m 7495 prarloc 7533 axaddcl 7894 axmulcl 7896 hashfacen 10851 bj-inex 15137 |
Copyright terms: Public domain | W3C validator |