![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimia | GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.) |
Ref | Expression |
---|---|
ralimia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
ralimia | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
2 | 1 | a2i 11 | . 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralimi2 2550 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 |
This theorem depends on definitions: df-bi 117 df-ral 2473 |
This theorem is referenced by: ralimiaa 2552 ralimi 2553 r19.12 2596 rr19.3v 2891 rr19.28v 2892 ffvresb 5700 f1mpt 5793 ixpf 6746 exmidontri2or 7272 peano2nnnn 7882 peano5nnnn 7921 peano5nni 8952 peano2nn 8961 serf0 11392 baspartn 14007 tridceq 15263 |
Copyright terms: Public domain | W3C validator |