Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralimdv | GIF version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.) |
Ref | Expression |
---|---|
ralimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | adantr 261 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 2387 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ 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: poss 4035 sess1 4074 sess2 4075 riinint 4593 dffo4 5315 dffo5 5316 isoini2 5458 rdgivallem 5968 iinerm 6178 resqrexlemgt0 9618 cau3lem 9710 caubnd2 9713 climshftlemg 9823 climcau 9866 climcaucn 9870 serif0 9871 |
Copyright terms: Public domain | W3C validator |