Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralrimivva | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.) |
Ref | Expression |
---|---|
ralrimivva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) |
Ref | Expression |
---|---|
ralrimivva | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimivva.1 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) | |
2 | 1 | ex 108 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) |
3 | 2 | ralrimivv 2400 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1393 ∀wral 2306 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 |
This theorem is referenced by: swopo 4043 sosng 4413 fcof1 5423 fliftfund 5437 isoresbr 5449 isocnv 5451 f1oiso 5465 caovclg 5653 caovcomg 5656 off 5724 caofrss 5735 fmpt2co 5837 poxp 5853 eroprf 6199 dom2lem 6252 nnwetri 6354 addlocpr 6634 mullocpr 6669 cauappcvgprlemloc 6750 cauappcvgprlemlim 6759 caucvgprlemloc 6773 caucvgprprlemloc 6801 rereceu 6963 cju 7913 qbtwnz 9106 frec2uzf1od 9192 frec2uzisod 9193 frecuzrdgrrn 9194 iseqcaopr3 9240 iseqcaopr2 9241 iseqhomo 9248 iseqdistr 9249 rsqrmo 9625 climcn2 9830 addcn2 9831 mulcn2 9833 |
Copyright terms: Public domain | W3C validator |