![]() |
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 113 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) |
3 | 2 | rexlimdvv 2488 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1434 ∃wrex 2354 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 ax-i5r 1469 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-ral 2358 df-rex 2359 |
This theorem is referenced by: ovelrn 5700 f1o2ndf1 5900 eroveu 6284 eroprf 6286 genipv 6796 genpelvl 6799 genpelvu 6800 genprndl 6808 genprndu 6809 addlocpr 6823 addnqprlemrl 6844 addnqprlemru 6845 mulnqprlemrl 6860 mulnqprlemru 6861 ltsopr 6883 ltaddpr 6884 ltexprlemfl 6896 ltexprlemrl 6897 ltexprlemfu 6898 ltexprlemru 6899 cauappcvgprlemladdfu 6941 cauappcvgprlemladdfl 6942 caucvgprlemdisj 6961 caucvgprlemladdfu 6964 caucvgprprlemdisj 6989 apreap 7789 apreim 7805 apirr 7807 apsym 7808 apcotr 7809 apadd1 7810 apneg 7813 mulext1 7814 apti 7824 qapne 8840 qtri3or 9364 exbtwnzlemex 9371 rebtwn2z 9376 cjap 9977 rexanre 10290 climcn2 10332 dvds2lem 10398 bezoutlemnewy 10575 bezoutlembi 10584 dvdsmulgcd 10604 divgcdcoprm0 10673 cncongr1 10675 sqrt2irrap 10748 |
Copyright terms: Public domain | W3C validator |