![]() |
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 1796. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 1876 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 1876 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1742 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem depends on definitions: df-bi 199 df-ex 1743 |
This theorem is referenced by: 2eu6 2689 cgsex2g 3453 cgsex4g 3454 spc2egv 3512 relop 5565 elinxp 5729 opreuopreu 7540 en3 8544 en4 8545 addsrpr 10289 mulsrpr 10290 hash2prde 13633 pmtrrn2 18343 umgredg 26620 umgr2wlkon 27450 fmla0xp 32193 fundmpss 32529 pellexlem5 38826 ax6e2eq 40310 fnchoice 40705 fzisoeu 40996 stoweidlem35 41751 stoweidlem60 41776 or2expropbi 42674 ich2exprop 43001 |
Copyright terms: Public domain | W3C validator |