![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > exlimdvv | GIF version |
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
exlimdvv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
exlimdvv | ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exlimdvv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | exlimdv 1819 | . 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒)) |
3 | 2 | exlimdv 1819 | 1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∃wex 1492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1447 ax-gen 1449 ax-ie2 1494 ax-17 1526 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: euotd 4250 funopg 5245 th3qlem1 6630 fundmen 6799 sbthlemi10 6958 addnq0mo 7424 mulnq0mo 7425 genprndl 7498 genprndu 7499 genpdisj 7500 mullocpr 7548 addsrmo 7720 mulsrmo 7721 cnm 7809 summodc 11362 fsum2dlemstep 11413 prodmodc 11557 fprod2dlemstep 11601 txbasval 13400 |
Copyright terms: Public domain | W3C validator |