![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2eximdv | Structured version Visualization version GIF version |
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1837. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 1921 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 1921 | 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: 2eu6 2653 cgsex2g 3520 cgsex4g 3521 cgsex4gOLD 3522 cgsex4gOLDOLD 3523 spc2egv 3590 rexopabb 5529 relop 5851 elinxp 6020 opreuopreu 8020 en3 9282 en4 9283 addsrpr 11070 mulsrpr 11071 hash2prde 14431 pmtrrn2 19328 umgredg 28398 umgr2wlkon 29204 trsp2cyc 32282 acycgrsubgr 34149 satfvsucsuc 34356 fmla0xp 34374 fundmpss 34738 pellexlem5 41571 ax6e2eq 43318 fnchoice 43713 fzisoeu 44010 stoweidlem35 44751 stoweidlem60 44776 or2expropbi 45744 ich2exprop 46139 |
Copyright terms: Public domain | W3C validator |