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 1738). (Contributed by AV, 27-Nov-2019.) |
Ref | Expression |
---|---|
ralimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdvva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdvva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
2 | 1 | anassrs 680 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 2962 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 → ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralimdva 2962 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ral 2917 |
This theorem is referenced by: dedekindle 10201 islmhm2 19038 dmatscmcl 20309 cpmatacl 20521 cpmatinvcl 20522 mat2pmatf1 20534 pmatcollpw2lem 20582 tgpt0 21922 isngp4 22416 addcnlem 22667 c1lip3 23762 aalioulem2 24088 aalioulem5 24091 aalioulem6 24092 aaliou 24093 iscgrglt 25409 2pthfrgrrn 27146 2pthfrgrrn2 27147 equivbnd 33589 ghomco 33690 |
Copyright terms: Public domain | W3C validator |