![]() |
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 1929. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 2013 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 2013 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 |
This theorem depends on definitions: df-bi 199 df-ex 1876 |
This theorem is referenced by: 2eu6 2714 cgsex2g 3427 cgsex4g 3428 spc2egv 3483 spc3egv 3485 relop 5476 elinxp 5644 elresOLD 5646 en3 8439 en4 8440 addsrpr 10184 mulsrpr 10185 hash2prde 13501 pmtrrn2 18192 umgredg 26374 umgr2wlkon 27239 fundmpss 32178 pellexlem5 38183 ax6e2eq 39543 fnchoice 39948 fzisoeu 40259 stoweidlem35 40995 stoweidlem60 41020 |
Copyright terms: Public domain | W3C validator |