![]() |
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 276 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 2544 | 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 ax-4 1510 ax-17 1526 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 |
This theorem is referenced by: poss 4300 sess1 4339 sess2 4340 riinint 4890 dffo4 5666 dffo5 5667 isoini2 5822 rdgivallem 6384 iinerm 6609 xpf1o 6846 exmidontriimlem3 7224 exmidontriim 7226 resqrexlemgt0 11031 cau3lem 11125 caubnd2 11128 climshftlemg 11312 climcau 11357 climcaucn 11361 serf0 11362 modfsummodlemstep 11467 bezoutlemmain 12001 ctinf 12433 strsetsid 12497 imasaddfnlemg 12740 islss4 13474 fiinbas 13588 baspartn 13589 lmtopcnp 13789 rescncf 14107 limcresi 14174 |
Copyright terms: Public domain | W3C validator |