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 1846 | . 2 ⊢ (𝜑 → ∀𝑦𝜓) |
3 | 2 | alrimiv 1846 | 1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1423 ax-gen 1425 ax-17 1506 |
This theorem is referenced by: 2ax17 1850 euind 2871 sbnfc2 3060 exmidsssn 4125 exmidel 4128 exmidundif 4129 exmidundifim 4130 ssopab2dv 4200 suctr 4343 eusvnf 4374 ordsuc 4478 ssrel 4627 relssdv 4631 eqrelrdv 4635 eqbrrdv 4636 eqrelrdv2 4638 ssrelrel 4639 iss 4865 funssres 5165 funun 5167 fununi 5191 fsn 5592 ovg 5909 caovimo 5964 oprabexd 6025 qliftfund 6512 eroveu 6520 th3qlem1 6531 exmidfodomrlemim 7057 addnq0mo 7255 mulnq0mo 7256 ltexprlemdisj 7414 recexprlemdisj 7438 addsrmo 7551 mulsrmo 7552 summodc 11152 prodmodc 11347 limcimo 12803 exmidsbth 13219 |
Copyright terms: Public domain | W3C validator |