![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimdvva | Structured version Visualization version GIF version |
Description: Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (Contributed by AV, 27-Nov-2019.) |
Ref | Expression |
---|---|
ralimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdvva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdvva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
2 | 1 | anassrs 466 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 3165 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralimdva 3165 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2104 ∀wral 3059 |
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-an 395 df-ral 3060 |
This theorem is referenced by: ralimdvv 3204 dedekindle 11382 islmhm2 20793 dflidl2lem 20991 dflidl2rng 21030 isdomn4 21118 dmatscmcl 22225 cpmatacl 22438 cpmatinvcl 22439 mat2pmatf1 22451 pmatcollpw2lem 22499 tgpt0 23843 isngp4 24341 addcnlem 24600 c1lip3 25751 aalioulem2 26082 aalioulem5 26085 aalioulem6 26086 aaliou 26087 iscgrglt 28032 2pthfrgrrn 29802 2pthfrgrrn2 29803 equivbnd 36961 ghomco 37062 fcoresf1 46077 fullthinc 47753 |
Copyright terms: Public domain | W3C validator |