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 2517 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2128 ∀wral 2435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 |
This theorem depends on definitions: df-bi 116 df-ral 2440 |
This theorem is referenced by: ralimiaa 2519 ralimi 2520 r19.12 2563 rr19.3v 2851 rr19.28v 2852 ffvresb 5630 f1mpt 5721 ixpf 6665 exmidontri2or 7178 peano2nnnn 7773 peano5nnnn 7812 peano5nni 8836 peano2nn 8845 serf0 11249 baspartn 12459 tridceq 13638 |
Copyright terms: Public domain | W3C validator |