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 1591 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1591 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1485 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1442 ax-ie2 1487 ax-17 1519 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: cgsex2g 2766 cgsex4g 2767 opabss 4051 copsexg 4227 elopab 4241 epelg 4273 0nelelxp 4638 elvvuni 4673 optocl 4685 xpsspw 4721 relopabi 4735 relop 4759 elreldm 4835 xpmlem 5029 dfco2a 5109 unielrel 5136 oprabid 5883 1stval2 6132 2ndval2 6133 xp1st 6142 xp2nd 6143 poxp 6209 rntpos 6234 dftpos4 6240 tpostpos 6241 tfrlem7 6294 th3qlem2 6613 ener 6754 domtr 6760 unen 6791 xpsnen 6796 mapen 6821 ltdcnq 7348 archnqq 7368 enq0tr 7385 nqnq0pi 7389 nqnq0 7392 nqpnq0nq 7404 nqnq0a 7405 nqnq0m 7406 nq0m0r 7407 nq0a0 7408 nq02m 7416 prarloc 7454 axaddcl 7815 axmulcl 7817 hashfacen 10760 bj-inex 13904 |
Copyright terms: Public domain | W3C validator |