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 2206. (Contributed by NM, 1-Aug-1995.) |
Ref | Expression |
---|---|
exlimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
exlimivv | ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | exlimiv 1927 | . 2 ⊢ (∃𝑦𝜑 → 𝜓) |
3 | 2 | exlimiv 1927 | 1 ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 |
This theorem depends on definitions: df-bi 209 df-ex 1777 |
This theorem is referenced by: cgsex2g 3539 cgsex4g 3540 opabss 5123 dtru 5264 copsexgw 5374 copsexg 5375 elopab 5407 elopabr 5440 epelgOLD 5462 0nelelxp 5585 elvvuni 5623 optocl 5640 relopabiALT 5690 relop 5716 elreldm 5800 xpnz 6011 xpdifid 6020 dfco2a 6094 unielrel 6120 unixp0 6129 funsndifnop 6908 fmptsng 6925 oprabidw 7181 oprabid 7182 oprabv 7208 1stval2 7700 2ndval2 7701 1st2val 7711 2nd2val 7712 xp1st 7715 xp2nd 7716 frxp 7814 poxp 7816 soxp 7817 rntpos 7899 dftpos4 7905 tpostpos 7906 wfrlem4 7952 wfrfun 7959 tfrlem7 8013 ener 8550 domtr 8556 unen 8590 xpsnen 8595 sbthlem10 8630 mapen 8675 djuunxp 9344 fseqen 9447 dfac5lem4 9546 kmlem16 9585 axdc4lem 9871 hashfacen 13806 hashle2pr 13829 fundmge2nop0 13844 gictr 18409 dvdsrval 19389 thlle 20835 hmphtr 22385 griedg0ssusgr 27041 rgrusgrprc 27365 numclwwlk1lem2fo 28131 frgrregord013 28168 friendship 28172 nvss 28364 spanuni 29315 5oalem7 29431 3oalem3 29435 opabssi 30358 gsummpt2co 30681 qqhval2 31218 bnj605 32174 bnj607 32183 funen1cnv 32352 loop1cycl 32379 satfv1 32605 sat1el2xp 32621 fmla0xp 32625 satefvfmla0 32660 mppspstlem 32813 mppsval 32814 frrlem4 33121 pprodss4v 33340 sscoid 33369 colinearex 33516 bj-dtru 34134 copsex2b 34426 sn-dtru 39104 pr2cv 39900 stoweidlem35 42313 funop1 43475 sprsymrelfvlem 43645 uspgrsprf 44014 uspgrsprf1 44015 rrx2plordisom 44703 |
Copyright terms: Public domain | W3C validator |