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 1751. (Contributed by NM, 3-Aug-1995.) |
Ref | Expression |
---|---|
2alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
2eximdv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2alimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | eximdv 1833 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → ∃𝑦𝜒)) |
3 | 2 | eximdv 1833 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: 2eu6 2546 cgsex2g 3212 cgsex4g 3213 spc2egv 3268 spc3egv 3270 relop 5194 elres 5355 en3 8082 en4 8083 addsrpr 9775 mulsrpr 9776 hash2prde 13109 pmtrrn2 17703 umgredg 25812 usgrarnedg 25913 fundmpss 30910 pellexlem5 36415 ax6e2eq 37794 fnchoice 38211 fzisoeu 38455 stoweidlem35 38928 stoweidlem60 38953 umgr2wlkon 41157 |
Copyright terms: Public domain | W3C validator |