![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > exlimdvv | Structured version Visualization version GIF version |
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2205. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
exlimdvv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
exlimdvv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimdvv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | exlimdv 1937 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒)) |
3 | 2 | exlimdv 1937 | 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: euotd 5513 opabssxpd 5722 dfpo2 6293 funopg 6580 fmptsnd 7164 tpres 7199 opreuopreu 8017 frxp2 8127 frxp3 8134 fundmen 9028 undomOLD 9057 ttrcltr 9708 infxpenc2 10014 zorn2lem6 10493 fpwwe2lem11 10633 genpnnp 10997 addsrmo 11065 mulsrmo 11066 hashfun 14394 hash2exprb 14429 rtrclreclem3 15004 summo 15660 fsum2dlem 15713 ntrivcvgmul 15845 prodmo 15877 fprod2dlem 15921 iscatd2 17622 gsumval3eu 19767 gsum2d2 19837 ptbasin 23073 txcls 23100 txbasval 23102 reconn 24336 phtpcer 24503 pcohtpy 24528 mbfi1flimlem 25232 mbfmullem 25235 itg2add 25269 fsumvma 26706 umgr3v3e3cycl 29427 conngrv2edg 29438 2ndresdju 31862 cusgracyclt3v 34136 pconnconn 34211 txsconn 34221 neibastop1 35233 itg2addnc 36531 riscer 36845 dalem62 38594 pellexlem5 41557 pellex 41559 nnoeomeqom 42048 iunrelexpuztr 42456 fzisoeu 43997 stoweidlem53 44756 stoweidlem56 44759 fundcmpsurinjpreimafv 46063 ichnreuop 46127 |
Copyright terms: Public domain | W3C validator |