Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exlimivv | Structured version Visualization version GIF version |
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2067. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1845 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1845 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: cgsex2g 3212 cgsex4g 3213 opabss 4646 dtru 4783 copsexg 4882 elopab 4908 elopabr 4937 epelg 4950 0nelelxp 5069 elvvuni 5102 optocl 5118 relopabiALT 5168 relop 5194 elreldm 5271 xpnz 5472 xpdifid 5481 dfco2a 5552 unielrel 5577 unixp0 5586 funsndifnop 6321 fmptsng 6339 oprabid 6576 oprabv 6601 1stval2 7076 2ndval2 7077 1st2val 7085 2nd2val 7086 xp1st 7089 xp2nd 7090 frxp 7174 poxp 7176 soxp 7177 rntpos 7252 dftpos4 7258 tpostpos 7259 wfrlem4 7305 wfrfun 7312 tfrlem7 7366 ener 7888 enerOLD 7889 domtr 7895 unen 7925 xpsnen 7929 sbthlem10 7964 mapen 8009 fseqen 8733 dfac5lem4 8832 kmlem16 8870 axdc4lem 9160 hashfacen 13095 fundmge2nop0 13129 gictr 17540 dvdsrval 18468 thlle 19860 hmphtr 21396 usgrac 25880 edgss 25881 cusgrarn 25988 3v3e3cycl2 26192 3v3e3cycl 26193 numclwlk1lem2fo 26622 frgraregord013 26645 friendship 26649 nvss 26832 spanuni 27787 5oalem7 27903 3oalem3 27907 gsummpt2co 29111 qqhval2 29354 bnj605 30231 bnj607 30240 mppspstlem 30722 mppsval 30723 frrlem4 31027 frrlem5c 31030 pprodss4v 31161 sscoid 31190 colinearex 31337 bj-dtru 31985 stoweidlem35 38928 funop1 40327 griedg0ssusgr 40489 rgrusgrprc 40789 av-numclwlk1lem2fo 41525 av-frgraregord013 41549 av-friendship 41553 |
Copyright terms: Public domain | W3C validator |