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 1577 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1577 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-gen 1425 ax-ie2 1470 ax-17 1506 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: cgsex2g 2722 cgsex4g 2723 opabss 3992 copsexg 4166 elopab 4180 epelg 4212 0nelelxp 4568 elvvuni 4603 optocl 4615 xpsspw 4651 relopabi 4665 relop 4689 elreldm 4765 xpmlem 4959 dfco2a 5039 unielrel 5066 oprabid 5803 1stval2 6053 2ndval2 6054 xp1st 6063 xp2nd 6064 poxp 6129 rntpos 6154 dftpos4 6160 tpostpos 6161 tfrlem7 6214 th3qlem2 6532 ener 6673 domtr 6679 unen 6710 xpsnen 6715 mapen 6740 ltdcnq 7205 archnqq 7225 enq0tr 7242 nqnq0pi 7246 nqnq0 7249 nqpnq0nq 7261 nqnq0a 7262 nqnq0m 7263 nq0m0r 7264 nq0a0 7265 nq02m 7273 prarloc 7311 axaddcl 7672 axmulcl 7674 hashfacen 10579 bj-inex 13105 |
Copyright terms: Public domain | W3C validator |