![]() |
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 2204. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1933 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1933 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1781 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-ex 1782 |
This theorem is referenced by: cgsex2g 3519 cgsex4g 3520 cgsex4gOLD 3521 cgsex4gOLDOLD 3522 opabss 5211 dtruALT2 5367 exneq 5434 dtruOLD 5440 copsexgw 5489 copsexg 5490 elopab 5526 elopabrOLD 5562 0nelelxp 5710 elvvuni 5750 optocl 5768 relopabiALT 5821 relop 5848 elreldm 5932 xpnz 6155 xpdifid 6164 dfco2a 6242 unielrel 6270 unixp0 6279 funsndifnop 7145 fmptsng 7162 oprabidw 7436 oprabid 7437 oprabv 7465 1stval2 7988 2ndval2 7989 1st2val 7999 2nd2val 8000 xp1st 8003 xp2nd 8004 frxp 8108 poxp 8110 soxp 8111 rntpos 8220 dftpos4 8226 tpostpos 8227 frrlem4 8270 wfrlem4OLD 8308 wfrfunOLD 8315 tfrlem7 8379 ener 8993 domtr 8999 unen 9042 xpsnen 9051 undom 9055 sbthlem10 9088 mapen 9137 cnvfi 9176 entrfil 9184 domtrfil 9191 sbthfilem 9197 djuunxp 9912 fseqen 10018 dfac5lem4 10117 kmlem16 10156 axdc4lem 10446 hashfacen 14409 hashfacenOLD 14410 hashle2pr 14434 fundmge2nop0 14449 catcone0 17627 gictr 19143 dvdsrval 20167 thlle 21242 thlleOLD 21243 hmphtr 23278 griedg0ssusgr 28511 rgrusgrprc 28835 numclwwlk1lem2fo 29600 frgrregord013 29637 friendship 29641 nvss 29833 spanuni 30784 5oalem7 30900 3oalem3 30904 opabssi 31829 gsummpt2co 32187 qqhval2 32950 bnj605 33906 bnj607 33915 funen1cnv 34079 fineqvac 34085 loop1cycl 34116 satfv1 34342 sat1el2xp 34358 fmla0xp 34362 satefvfmla0 34397 mppspstlem 34550 mppsval 34551 pprodss4v 34844 sscoid 34873 colinearex 35020 copsex2b 36009 rictr 41092 pr2cv 42284 stoweidlem35 44737 funop1 45977 sprsymrelfvlem 46144 uspgrsprf 46510 uspgrsprf1 46511 rngqiprngimfo 46766 rrx2plordisom 47362 |
Copyright terms: Public domain | W3C validator |