![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alrimivv | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
alrimivv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimivv | ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimivv.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | alrimiv 1803 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1803 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1288 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-5 1382 ax-gen 1384 ax-17 1465 |
This theorem is referenced by: 2ax17 1807 euind 2803 sbnfc2 2989 exmidsssn 4040 exmidel 4042 exmidundif 4043 exmidundifim 4044 ssopab2dv 4114 suctr 4257 eusvnf 4288 ordsuc 4392 ssrel 4539 relssdv 4543 eqrelrdv 4547 eqbrrdv 4548 eqrelrdv2 4550 ssrelrel 4551 iss 4771 funssres 5069 funun 5071 fununi 5095 fsn 5483 ovg 5797 caovimo 5852 oprabexd 5912 qliftfund 6389 eroveu 6397 th3qlem1 6408 exmidfodomrlemim 6888 addnq0mo 7067 mulnq0mo 7068 ltexprlemdisj 7226 recexprlemdisj 7250 addsrmo 7350 mulsrmo 7351 isummo 10834 exmidsbth 12186 |
Copyright terms: Public domain | W3C validator |