![]() |
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 1885 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1885 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1458 ax-gen 1460 ax-17 1537 |
This theorem is referenced by: 2ax17 1889 euind 2939 sbnfc2 3132 exmidsssn 4217 exmidel 4220 exmidundif 4221 exmidundifim 4222 ssopab2dv 4293 suctr 4436 eusvnf 4468 ordsuc 4577 ssrel 4729 relssdv 4733 eqrelrdv 4737 eqbrrdv 4738 eqrelrdv2 4740 ssrelrel 4741 iss 4968 funssres 5273 funun 5275 fununi 5299 fsn 5704 ovg 6030 caovimo 6085 oprabexd 6146 qliftfund 6636 eroveu 6644 th3qlem1 6655 exmidfodomrlemim 7218 exmidmotap 7278 addnq0mo 7464 mulnq0mo 7465 ltexprlemdisj 7623 recexprlemdisj 7647 addsrmo 7760 mulsrmo 7761 summodc 11409 prodmodc 11604 pceu 12313 rhmex 13468 limcimo 14531 exmidsbth 15170 |
Copyright terms: Public domain | W3C validator |