|   | 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 1809). (Contributed by AV, 27-Nov-2019.) | 
| Ref | Expression | 
|---|---|
| ralimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | 
| Ref | Expression | 
|---|---|
| ralimdvva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ralimdvva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
| 2 | 1 | anassrs 467 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) | 
| 3 | 2 | ralimdva 3166 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒)) | 
| 4 | 3 | ralimdva 3166 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3061 | 
| This theorem is referenced by: ralimdvv 3207 dedekindle 11426 isdomn4 20717 islmhm2 21038 dflidl2rng 21229 dmatscmcl 22510 cpmatacl 22723 cpmatinvcl 22724 mat2pmatf1 22736 pmatcollpw2lem 22784 tgpt0 24128 isngp4 24626 addcnlem 24887 c1lip3 26039 aalioulem2 26376 aalioulem5 26379 aalioulem6 26380 aaliou 26381 iscgrglt 28523 2pthfrgrrn 30302 2pthfrgrrn2 30303 equivbnd 37798 ghomco 37899 fcoresf1 47086 fullthinc 49124 | 
| Copyright terms: Public domain | W3C validator |