![]() |
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 2205. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1934 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1934 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1782 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: cgsex2g 3492 cgsex4g 3493 cgsex4gOLD 3494 opabss 5174 dtruALT2 5330 exneq 5397 dtruOLD 5403 copsexgw 5452 copsexg 5453 elopab 5489 elopabrOLD 5525 0nelelxp 5673 elvvuni 5713 optocl 5731 relopabiALT 5784 relop 5811 elreldm 5895 xpnz 6116 xpdifid 6125 dfco2a 6203 unielrel 6231 unixp0 6240 funsndifnop 7102 fmptsng 7119 oprabidw 7393 oprabid 7394 oprabv 7422 1stval2 7943 2ndval2 7944 1st2val 7954 2nd2val 7955 xp1st 7958 xp2nd 7959 frxp 8063 poxp 8065 soxp 8066 rntpos 8175 dftpos4 8181 tpostpos 8182 frrlem4 8225 wfrlem4OLD 8263 wfrfunOLD 8270 tfrlem7 8334 ener 8948 domtr 8954 unen 8997 xpsnen 9006 undom 9010 sbthlem10 9043 mapen 9092 cnvfi 9131 entrfil 9139 domtrfil 9146 sbthfilem 9152 djuunxp 9864 fseqen 9970 dfac5lem4 10069 kmlem16 10108 axdc4lem 10398 hashfacen 14358 hashfacenOLD 14359 hashle2pr 14383 fundmge2nop0 14398 catcone0 17574 gictr 19072 dvdsrval 20081 thlle 21118 thlleOLD 21119 hmphtr 23150 griedg0ssusgr 28255 rgrusgrprc 28579 numclwwlk1lem2fo 29344 frgrregord013 29381 friendship 29385 nvss 29577 spanuni 30528 5oalem7 30644 3oalem3 30648 opabssi 31574 gsummpt2co 31932 qqhval2 32603 bnj605 33559 bnj607 33568 funen1cnv 33732 fineqvac 33738 loop1cycl 33771 satfv1 33997 sat1el2xp 34013 fmla0xp 34017 satefvfmla0 34052 mppspstlem 34205 mppsval 34206 pprodss4v 34498 sscoid 34527 colinearex 34674 copsex2b 35640 rictr 40731 pr2cv 41894 stoweidlem35 44350 funop1 45589 sprsymrelfvlem 45756 uspgrsprf 46122 uspgrsprf1 46123 rrx2plordisom 46883 |
Copyright terms: Public domain | W3C validator |