Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimivv | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
Ref | Expression |
---|---|
rexlimivv.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimivv | ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivv.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) | |
2 | 1 | rexlimdva 2581 | . 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | rexlimiv 2575 | 1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2135 ∃wrex 2443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-i5r 1522 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 df-rex 2448 |
This theorem is referenced by: opelxp 4631 f1o2ndf1 6190 xpdom2 6791 distrlem5prl 7521 distrlem5pru 7522 mulid1 7890 cnegex 8070 recexap 8544 creur 8848 creui 8849 cju 8850 elz2 9256 qre 9557 qaddcl 9567 qnegcl 9568 qmulcl 9569 qreccl 9574 elpqb 9581 replim 10795 prodmodc 11513 odd2np1 11804 opoe 11826 omoe 11827 opeo 11828 omeo 11829 qredeu 12023 pythagtriplem1 12191 pcz 12257 4sqlem1 12312 4sqlem2 12313 4sqlem4 12316 mul4sq 12318 txuni2 12854 blssioo 13143 tgioo 13144 |
Copyright terms: Public domain | W3C validator |