![]() |
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 2537 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ∀wral 2455 |
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 1447 ax-gen 1449 |
This theorem depends on definitions: df-bi 117 df-ral 2460 |
This theorem is referenced by: ralimiaa 2539 ralimi 2540 r19.12 2583 rr19.3v 2876 rr19.28v 2877 ffvresb 5679 f1mpt 5771 ixpf 6719 exmidontri2or 7241 peano2nnnn 7851 peano5nnnn 7890 peano5nni 8921 peano2nn 8930 serf0 11359 baspartn 13520 tridceq 14774 |
Copyright terms: Public domain | W3C validator |