![]() |
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 1831. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 1915 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 1915 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 |
This theorem depends on definitions: df-bi 207 df-ex 1777 |
This theorem is referenced by: 2eu6 2655 cgsex2g 3525 cgsex4g 3526 cgsex4gOLD 3527 spc2egv 3599 rexopabb 5538 relop 5864 elinxp 6039 opreuopreu 8058 en3 9314 en4 9315 addsrpr 11113 mulsrpr 11114 hash2prde 14506 hash3tpde 14529 pmtrrn2 19493 umgredg 29170 umgr2wlkon 29980 trsp2cyc 33126 acycgrsubgr 35143 satfvsucsuc 35350 fmla0xp 35368 fundmpss 35748 pellexlem5 42821 ax6e2eq 44555 fnchoice 44967 fzisoeu 45251 stoweidlem35 45991 stoweidlem60 46016 or2expropbi 46984 ich2exprop 47396 |
Copyright terms: Public domain | W3C validator |