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 1867 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1867 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1440 ax-gen 1442 ax-17 1519 |
This theorem is referenced by: 2ax17 1871 euind 2917 sbnfc2 3109 exmidsssn 4188 exmidel 4191 exmidundif 4192 exmidundifim 4193 ssopab2dv 4263 suctr 4406 eusvnf 4438 ordsuc 4547 ssrel 4699 relssdv 4703 eqrelrdv 4707 eqbrrdv 4708 eqrelrdv2 4710 ssrelrel 4711 iss 4937 funssres 5240 funun 5242 fununi 5266 fsn 5668 ovg 5991 caovimo 6046 oprabexd 6106 qliftfund 6596 eroveu 6604 th3qlem1 6615 exmidfodomrlemim 7178 addnq0mo 7409 mulnq0mo 7410 ltexprlemdisj 7568 recexprlemdisj 7592 addsrmo 7705 mulsrmo 7706 summodc 11346 prodmodc 11541 pceu 12249 limcimo 13428 exmidsbth 14056 |
Copyright terms: Public domain | W3C validator |