![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > r19.21bi | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) |
Ref | Expression |
---|---|
r19.21bi.1 | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Ref | Expression |
---|---|
r19.21bi | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.21bi.1 | . . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | |
2 | df-ral 2365 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
3 | 1, 2 | sylib 121 | . . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | 3 | 19.21bi 1496 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
5 | 4 | imp 123 | 1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∀wal 1288 ∈ wcel 1439 ∀wral 2360 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-4 1446 |
This theorem depends on definitions: df-bi 116 df-ral 2365 |
This theorem is referenced by: rspec2 2463 rspec3 2464 r19.21be 2465 frind 4188 wepo 4195 wetrep 4196 ordelord 4217 ralxfr2d 4299 rexxfr2d 4300 funfveu 5331 f1oresrab 5477 isoselem 5613 disjxp1 6015 tfrlemisucaccv 6104 tfr1onlemsucaccv 6120 tfrcllemsucaccv 6133 xpf1o 6614 fimax2gtrilemstep 6670 supisoti 6759 exmidomni 6859 prcdnql 7104 prcunqu 7105 prdisj 7112 caucvgsrlembound 7400 caucvgsrlemoffgt1 7405 exbtwnzlemex 9722 monoord2 9966 iseqf1olemqk 9984 seq3f1olemqsumk 9989 caucvgrelemcau 10474 fimaxre2 10719 climrecvg1n 10798 zisum 10835 fisum 10839 isumss2 10846 fisumser 10851 sumpr 10868 sumtp 10869 fsum2dlemstep 10889 fsumiun 10932 isumlessdc 10951 bezoutlemstep 11325 |
Copyright terms: Public domain | W3C validator |