![]() |
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 2364 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
3 | 1, 2 | sylib 120 | . . 3 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) |
4 | 3 | 19.21bi 1495 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
5 | 4 | imp 122 | 1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∀wal 1287 ∈ wcel 1438 ∀wral 2359 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-4 1445 |
This theorem depends on definitions: df-bi 115 df-ral 2364 |
This theorem is referenced by: rspec2 2462 rspec3 2463 r19.21be 2464 frind 4179 wepo 4186 wetrep 4187 ordelord 4208 ralxfr2d 4286 rexxfr2d 4287 funfveu 5318 f1oresrab 5463 isoselem 5599 disjxp1 6001 tfrlemisucaccv 6090 tfr1onlemsucaccv 6106 tfrcllemsucaccv 6119 xpf1o 6560 fimax2gtrilemstep 6616 supisoti 6705 exmidomni 6798 prcdnql 7043 prcunqu 7044 prdisj 7051 caucvgsrlembound 7339 caucvgsrlemoffgt1 7344 exbtwnzlemex 9661 monoord2 9905 iseqf1olemqk 9923 seq3f1olemqsumk 9928 caucvgrelemcau 10413 fimaxre2 10658 climrecvg1n 10737 zisum 10774 fisum 10778 isumss2 10785 fisumser 10790 sumpr 10807 sumtp 10808 fsum2dlemstep 10828 fsumiun 10871 isumlessdc 10890 bezoutlemstep 11264 |
Copyright terms: Public domain | W3C validator |