![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimdv | GIF version |
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
exlimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
exlimdv | ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1537 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | ax-17 1537 | . 2 ⊢ (𝜒 → ∀𝑥𝜒) | |
3 | exlimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 1, 2, 3 | exlimdh 1607 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1503 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1458 ax-gen 1460 ax-ie2 1505 ax-17 1537 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: ax11v2 1831 exlimdvv 1909 exlimddv 1910 tpid3g 3722 sssnm 3769 pwntru 4214 euotd 4269 ralxfr2d 4479 rexxfr2d 4480 releldmb 4879 relelrnb 4880 elres 4958 iss 4968 imain 5314 elunirn 5784 ovmpt4g 6015 oprssdmm 6191 op1steq 6199 fo2ndf 6247 reldmtpos 6273 rntpos 6277 tfrlemibacc 6346 tfrlemibxssdm 6347 tfrlemibfn 6348 tfrexlem 6354 tfr1onlembacc 6362 tfr1onlembxssdm 6363 tfr1onlembfn 6364 tfrcllembacc 6375 tfrcllembxssdm 6376 tfrcllembfn 6377 map0g 6709 xpdom3m 6855 phplem4 6878 phpm 6888 findcard2 6912 findcard2s 6913 ac6sfi 6921 fiintim 6952 xpfi 6953 fidcenum 6980 ordiso 7060 ctmlemr 7132 ctm 7133 ctssdc 7137 pm54.43 7214 exmidfodomrlemim 7225 recclnq 7416 ltexnqq 7432 ltbtwnnqq 7439 recexprlemss1l 7659 recexprlemss1u 7660 negm 9640 ioom 10286 seq3f1olemp 10528 fiinfnf1o 10793 fihashf1rn 10795 climcau 11382 summodclem2 11417 zsumdc 11419 isumz 11424 fsumf1o 11425 fisumss 11427 fsumcl2lem 11433 fsumadd 11441 fsummulc2 11483 ntrivcvgap 11583 prodmodclem2 11612 zproddc 11614 prod1dc 11621 fprodf1o 11623 fprodssdc 11625 fprodmul 11626 nnmindc 12062 uzwodc 12065 pceu 12322 4sqlemafi 12422 4sqlem12 12429 ennnfone 12471 enctlem 12478 unct 12488 sgrpidmndm 12874 subrngintm 13552 subrgintm 13583 islssm 13666 lss0cl 13678 islidlm 13788 eltg3 13994 tgtop 14005 tgidm 14011 tgrest 14106 tgcn 14145 xblm 14354 dvfgg 14594 dvcnp2cntop 14600 pwtrufal 15185 |
Copyright terms: Public domain | W3C validator |