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 1854 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1854 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1427 ax-gen 1429 ax-17 1506 |
This theorem is referenced by: 2ax17 1858 euind 2899 sbnfc2 3091 exmidsssn 4163 exmidel 4166 exmidundif 4167 exmidundifim 4168 ssopab2dv 4238 suctr 4381 eusvnf 4413 ordsuc 4522 ssrel 4674 relssdv 4678 eqrelrdv 4682 eqbrrdv 4683 eqrelrdv2 4685 ssrelrel 4686 iss 4912 funssres 5212 funun 5214 fununi 5238 fsn 5639 ovg 5959 caovimo 6014 oprabexd 6075 qliftfund 6563 eroveu 6571 th3qlem1 6582 exmidfodomrlemim 7136 addnq0mo 7367 mulnq0mo 7368 ltexprlemdisj 7526 recexprlemdisj 7550 addsrmo 7663 mulsrmo 7664 summodc 11280 prodmodc 11475 limcimo 13034 exmidsbth 13595 |
Copyright terms: Public domain | W3C validator |