| 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 2249. (Contributed by NM, 31-Jul-1995.) |
| Ref | Expression |
|---|---|
| exlimdvv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| exlimdvv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exlimdvv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 1 | exlimdv 1956 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒)) |
| 3 | 2 | exlimdv 1956 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∃wex 1802 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 |
| This theorem depends on definitions: df-bi 210 df-ex 1803 |
| This theorem is referenced by: euotd 5486 brab2d 5512 opabssxpd 5698 dfpo2 6286 funopg 6559 fmptsnd 7157 tpres 7189 opreuopreu 8019 frxp2 8128 frxp3 8135 fundmen 9016 ttrcltr 9673 infxpenc2 9994 zorn2lem6 10473 fpwwe2lem11 10614 genpnnp 10978 addsrmo 11046 mulsrmo 11047 hashfun 14462 hash2exprb 14496 hash3tpexb 14519 rtrclreclem3 15085 summo 15756 fsum2dlem 15809 ntrivcvgmul 15944 prodmo 15978 fprod2dlem 16022 iscatd2 17725 gsumval3eu 19962 gsum2d2 20032 ptbasin 23691 txcls 23718 txbasval 23720 reconn 24943 phtpcer 25111 pcohtpy 25136 mbfi1flimlem 25838 mbfmullem 25841 itg2add 25875 fsumvma 27331 umgr3v3e3cycl 30440 conngrv2edg 30451 2ndresdju 32902 cusgracyclt3v 35514 pconnconn 35589 txsconn 35599 neibastop1 36727 cgsex2gd 37636 itg2addnc 38180 riscer 38494 dalem62 40365 pellexlem5 43417 pellex 43419 nnoeomeqom 43896 iunrelexpuztr 44302 fzisoeu 45878 stoweidlem53 46626 stoweidlem56 46629 fundcmpsurinjpreimafv 48013 ichnreuop 48077 cycldlenngric 48549 brab2dd 49458 |
| Copyright terms: Public domain | W3C validator |