| 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 2573 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2176 ∀wral 2484 |
| 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 1470 ax-gen 1472 ax-4 1533 ax-17 1549 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 df-ral 2489 |
| This theorem is referenced by: poss 4345 sess1 4384 sess2 4385 riinint 4939 dffo4 5728 dffo5 5729 isoini2 5888 rdgivallem 6467 iinerm 6694 xpf1o 6941 exmidontriimlem3 7335 exmidontriim 7337 resqrexlemgt0 11331 cau3lem 11425 caubnd2 11428 climshftlemg 11613 climcau 11658 climcaucn 11662 serf0 11663 modfsummodlemstep 11768 bezoutlemmain 12319 ctinf 12801 strsetsid 12865 imasaddfnlemg 13146 islss4 14144 fiinbas 14521 baspartn 14522 lmtopcnp 14722 rescncf 15053 limcresi 15138 |
| Copyright terms: Public domain | W3C validator |