![]() |
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 1474 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | ax-17 1474 | . 2 ⊢ (𝜒 → ∀𝑥𝜒) | |
3 | exlimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 1, 2, 3 | exlimdh 1543 | 1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1436 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-5 1391 ax-gen 1393 ax-ie2 1438 ax-17 1474 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v2 1759 exlimdvv 1836 exlimddv 1837 tpid3g 3585 sssnm 3628 euotd 4114 ralxfr2d 4323 rexxfr2d 4324 releldmb 4714 relelrnb 4715 elres 4791 iss 4801 imain 5141 elunirn 5599 ovmpt4g 5825 op1steq 6007 fo2ndf 6054 reldmtpos 6080 rntpos 6084 tfrlemibacc 6153 tfrlemibxssdm 6154 tfrlemibfn 6155 tfrexlem 6161 tfr1onlembacc 6169 tfr1onlembxssdm 6170 tfr1onlembfn 6171 tfrcllembacc 6182 tfrcllembxssdm 6183 tfrcllembfn 6184 map0g 6512 xpdom3m 6657 phplem4 6678 phpm 6688 findcard2 6712 findcard2s 6713 ac6sfi 6721 fiintim 6746 xpfi 6747 fidcenum 6772 ordiso 6836 ctmlemr 6908 ctm 6909 ctssdc 6912 pm54.43 6957 exmidfodomrlemim 6966 recclnq 7101 ltexnqq 7117 ltbtwnnqq 7124 recexprlemss1l 7344 recexprlemss1u 7345 negm 9257 ioom 9879 seq3f1olemp 10116 fiinfnf1o 10373 fihashf1rn 10376 climcau 10955 summodclem2 10990 zsumdc 10992 isumz 10997 fsumf1o 10998 fisumss 11000 fsumcl2lem 11006 fsumadd 11014 fsummulc2 11056 ennnfone 11730 eltg3 12008 tgtop 12019 tgidm 12025 tgrest 12120 tgcn 12158 xblm 12345 dvfgg 12530 pwtrufal 12777 pwntru 12778 |
Copyright terms: Public domain | W3C validator |