![]() |
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 1834. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 1918 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 1918 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 |
This theorem depends on definitions: df-bi 206 df-ex 1780 |
This theorem is referenced by: 2eu6 2650 cgsex2g 3518 cgsex4g 3519 cgsex4gOLD 3520 cgsex4gOLDOLD 3521 spc2egv 3588 rexopabb 5527 relop 5849 elinxp 6018 opreuopreu 8022 en3 9284 en4 9285 addsrpr 11072 mulsrpr 11073 hash2prde 14435 pmtrrn2 19369 umgredg 28665 umgr2wlkon 29471 trsp2cyc 32552 acycgrsubgr 34447 satfvsucsuc 34654 fmla0xp 34672 fundmpss 35042 pellexlem5 41873 ax6e2eq 43620 fnchoice 44015 fzisoeu 44308 stoweidlem35 45049 stoweidlem60 45074 or2expropbi 46042 ich2exprop 46437 |
Copyright terms: Public domain | W3C validator |