![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximdai | Structured version Visualization version GIF version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.) |
Ref | Expression |
---|---|
reximdai.1 | ⊢ Ⅎ𝑥𝜑 |
reximdai.2 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
reximdai | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdai.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | reximdai.2 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
3 | 1, 2 | ralrimi 3249 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
4 | rexim 3082 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1778 ∈ wcel 2099 ∀wral 3056 ∃wrex 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-12 2164 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-nf 1779 df-ral 3057 df-rex 3066 |
This theorem is referenced by: 2reurex 3753 fompt 7122 tz7.49 8459 hsmexlem2 10444 acunirnmpt2 32439 acunirnmpt2f 32440 locfinreflem 33431 cmpcref 33441 fvineqsneq 36881 indexdom 37196 filbcmb 37202 cdlemefr29exN 39864 rexanuz3 44434 reximdd 44490 disjrnmpt2 44533 disjinfi 44537 iunmapsn 44562 infnsuprnmpt 44598 rnmptbdlem 44603 supxrge 44692 suplesup 44693 infxr 44721 allbutfi 44747 supxrunb3 44753 infxrunb3rnmpt 44782 infrpgernmpt 44819 limsupre 45001 limsupub 45064 limsupre3lem 45092 limsupgtlem 45137 xlimmnfvlem1 45192 xlimpnfvlem1 45196 stoweidlem31 45391 stoweidlem34 45394 fourierdlem73 45539 sge0pnffigt 45756 sge0ltfirp 45760 sge0reuzb 45808 iundjiun 45820 ovnlerp 45922 smflimlem4 46134 smflimsuplem7 46186 |
Copyright terms: Public domain | W3C validator |