Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimdvva | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
rexlimdvva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvva.1 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
2 | 1 | ex 108 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) |
3 | 2 | rexlimdvv 2439 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1393 ∃wrex 2307 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 df-rex 2312 |
This theorem is referenced by: ovelrn 5649 f1o2ndf1 5849 eroveu 6197 eroprf 6199 genipv 6607 genpelvl 6610 genpelvu 6611 genprndl 6619 genprndu 6620 addlocpr 6634 addnqprlemrl 6655 addnqprlemru 6656 mulnqprlemrl 6671 mulnqprlemru 6672 ltsopr 6694 ltaddpr 6695 ltexprlemfl 6707 ltexprlemrl 6708 ltexprlemfu 6709 ltexprlemru 6710 cauappcvgprlemladdfu 6752 cauappcvgprlemladdfl 6753 caucvgprlemdisj 6772 caucvgprlemladdfu 6775 caucvgprprlemdisj 6800 apreap 7578 apreim 7594 apirr 7596 apsym 7597 apcotr 7598 apadd1 7599 apneg 7602 mulext1 7603 apti 7613 qapne 8574 qtri3or 9098 qbtwnzlemex 9105 rebtwn2z 9109 cjap 9506 climcn2 9830 |
Copyright terms: Public domain | W3C validator |