| 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 2211. (Contributed by NM, 31-Jul-1995.) |
| Ref | Expression |
|---|---|
| exlimdvv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| exlimdvv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exlimdvv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 1 | exlimdv 1933 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒)) |
| 3 | 2 | exlimdv 1933 | 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 1910 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: euotd 5518 opabssxpd 5732 dfpo2 6316 funopg 6600 fmptsnd 7189 tpres 7221 opreuopreu 8059 frxp2 8169 frxp3 8176 fundmen 9071 undomOLD 9100 ttrcltr 9756 infxpenc2 10062 zorn2lem6 10541 fpwwe2lem11 10681 genpnnp 11045 addsrmo 11113 mulsrmo 11114 hashfun 14476 hash2exprb 14510 hash3tpexb 14533 rtrclreclem3 15099 summo 15753 fsum2dlem 15806 ntrivcvgmul 15938 prodmo 15972 fprod2dlem 16016 iscatd2 17724 gsumval3eu 19922 gsum2d2 19992 ptbasin 23585 txcls 23612 txbasval 23614 reconn 24850 phtpcer 25027 pcohtpy 25053 mbfi1flimlem 25757 mbfmullem 25760 itg2add 25794 fsumvma 27257 umgr3v3e3cycl 30203 conngrv2edg 30214 brab2d 32619 2ndresdju 32659 cusgracyclt3v 35161 pconnconn 35236 txsconn 35246 neibastop1 36360 itg2addnc 37681 riscer 37995 dalem62 39736 pellexlem5 42844 pellex 42846 nnoeomeqom 43325 iunrelexpuztr 43732 fzisoeu 45312 stoweidlem53 46068 stoweidlem56 46071 fundcmpsurinjpreimafv 47395 ichnreuop 47459 brab2dd 48741 |
| Copyright terms: Public domain | W3C validator |