![]() |
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 1813). (Contributed by AV, 27-Nov-2019.) |
Ref | Expression |
---|---|
ralimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdvva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdvva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
2 | 1 | anassrs 469 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 3168 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralimdva 3168 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3062 |
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-an 398 df-ral 3063 |
This theorem is referenced by: ralimdvv 3207 dedekindle 11378 islmhm2 20649 dflidl2lem 20842 isdomn4 20918 dmatscmcl 22005 cpmatacl 22218 cpmatinvcl 22219 mat2pmatf1 22231 pmatcollpw2lem 22279 tgpt0 23623 isngp4 24121 addcnlem 24380 c1lip3 25516 aalioulem2 25846 aalioulem5 25849 aalioulem6 25850 aaliou 25851 iscgrglt 27765 2pthfrgrrn 29535 2pthfrgrrn2 29536 equivbnd 36658 ghomco 36759 fcoresf1 45779 dflidl2rng 46750 fullthinc 47666 |
Copyright terms: Public domain | W3C validator |