![]() |
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 2557 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ∀wral 2468 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: poss 4316 sess1 4355 sess2 4356 riinint 4906 dffo4 5685 dffo5 5686 isoini2 5841 rdgivallem 6406 iinerm 6633 xpf1o 6872 exmidontriimlem3 7252 exmidontriim 7254 resqrexlemgt0 11061 cau3lem 11155 caubnd2 11158 climshftlemg 11342 climcau 11387 climcaucn 11391 serf0 11392 modfsummodlemstep 11497 bezoutlemmain 12031 ctinf 12481 strsetsid 12545 imasaddfnlemg 12791 islss4 13698 fiinbas 14006 baspartn 14007 lmtopcnp 14207 rescncf 14525 limcresi 14592 |
Copyright terms: Public domain | W3C validator |