| 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 2572 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2175 ∀wral 2483 |
| 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 1469 ax-gen 1471 ax-4 1532 ax-17 1548 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 df-ral 2488 |
| This theorem is referenced by: poss 4344 sess1 4383 sess2 4384 riinint 4938 dffo4 5727 dffo5 5728 isoini2 5887 rdgivallem 6466 iinerm 6693 xpf1o 6940 exmidontriimlem3 7334 exmidontriim 7336 resqrexlemgt0 11302 cau3lem 11396 caubnd2 11399 climshftlemg 11584 climcau 11629 climcaucn 11633 serf0 11634 modfsummodlemstep 11739 bezoutlemmain 12290 ctinf 12772 strsetsid 12836 imasaddfnlemg 13117 islss4 14115 fiinbas 14492 baspartn 14493 lmtopcnp 14693 rescncf 15024 limcresi 15109 |
| Copyright terms: Public domain | W3C validator |