![]() |
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 2657 cgsex2g 3492 cgsex4g 3493 cgsex4gOLD 3494 spc2egv 3561 rexopabb 5490 relop 5811 elinxp 5980 opreuopreu 7971 en3 9233 en4 9234 addsrpr 11018 mulsrpr 11019 hash2prde 14376 pmtrrn2 19249 umgredg 28131 umgr2wlkon 28937 trsp2cyc 32014 acycgrsubgr 33792 satfvsucsuc 33999 fmla0xp 34017 fundmpss 34380 pellexlem5 41185 ax6e2eq 42913 fnchoice 43308 fzisoeu 43608 stoweidlem35 44350 stoweidlem60 44375 or2expropbi 45342 ich2exprop 45737 |
Copyright terms: Public domain | W3C validator |