![]() |
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 274 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 2521 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2125 ∀wral 2432 |
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 1424 ax-gen 1426 ax-4 1487 ax-17 1503 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-ral 2437 |
This theorem is referenced by: poss 4253 sess1 4292 sess2 4293 riinint 4840 dffo4 5608 dffo5 5609 isoini2 5760 rdgivallem 6318 iinerm 6541 xpf1o 6778 exmidontriimlem3 7137 exmidontriim 7139 resqrexlemgt0 10897 cau3lem 10991 caubnd2 10994 climshftlemg 11176 climcau 11221 climcaucn 11225 serf0 11226 modfsummodlemstep 11331 bezoutlemmain 11853 ctinf 12110 strsetsid 12162 fiinbas 12386 baspartn 12387 lmtopcnp 12589 rescncf 12907 limcresi 12974 |
Copyright terms: Public domain | W3C validator |