![]() |
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 2202. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1931 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1931 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 |
This theorem depends on definitions: df-bi 206 df-ex 1780 |
This theorem is referenced by: cgsex2g 3518 cgsex4g 3519 cgsex4gOLD 3520 cgsex4gOLDOLD 3521 opabss 5211 dtruALT2 5367 exneq 5434 dtruOLD 5440 copsexgw 5489 copsexg 5490 elopab 5526 elopabrOLD 5562 0nelelxp 5710 elvvuni 5751 optocl 5769 relopabiALT 5822 relop 5849 elreldm 5933 xpnz 6157 xpdifid 6166 dfco2a 6244 unielrel 6272 unixp0 6281 funsndifnop 7150 fmptsng 7167 oprabidw 7442 oprabid 7443 oprabv 7471 1stval2 7994 2ndval2 7995 1st2val 8005 2nd2val 8006 xp1st 8009 xp2nd 8010 frxp 8114 poxp 8116 soxp 8117 rntpos 8226 dftpos4 8232 tpostpos 8233 frrlem4 8276 wfrlem4OLD 8314 wfrfunOLD 8321 tfrlem7 8385 ener 8999 domtr 9005 unen 9048 xpsnen 9057 undom 9061 sbthlem10 9094 mapen 9143 cnvfi 9182 entrfil 9190 domtrfil 9197 sbthfilem 9203 djuunxp 9918 fseqen 10024 dfac5lem4 10123 kmlem16 10162 axdc4lem 10452 hashfacen 14417 hashfacenOLD 14418 hashle2pr 14442 fundmge2nop0 14457 catcone0 17635 gictr 19190 dvdsrval 20252 rngqiprngimfo 21060 thlle 21470 thlleOLD 21471 hmphtr 23507 griedg0ssusgr 28789 rgrusgrprc 29113 numclwwlk1lem2fo 29878 frgrregord013 29915 friendship 29919 nvss 30113 spanuni 31064 5oalem7 31180 3oalem3 31184 opabssi 32109 gsummpt2co 32470 qqhval2 33260 bnj605 34216 bnj607 34225 funen1cnv 34389 fineqvac 34395 loop1cycl 34426 satfv1 34652 sat1el2xp 34668 fmla0xp 34672 satefvfmla0 34707 mppspstlem 34860 mppsval 34861 pprodss4v 35160 sscoid 35189 colinearex 35336 copsex2b 36324 rictr 41399 pr2cv 42601 stoweidlem35 45049 funop1 46289 sprsymrelfvlem 46456 uspgrsprf 46822 uspgrsprf1 46823 rrx2plordisom 47496 |
Copyright terms: Public domain | W3C validator |