Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alrimiv | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
alrimiv.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimiv | ⊢ (𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1419 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alrimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | alrimih 1358 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-5 1336 ax-gen 1338 ax-17 1419 |
This theorem is referenced by: alrimivv 1755 nfdv 1757 axext4 2024 eqrdv 2038 abbi2dv 2156 abbi1dv 2157 elex22 2569 elex2 2570 spcimdv 2637 spcimedv 2639 pm13.183 2681 sbcthdv 2778 sbcimdv 2823 ssrdv 2951 ss2abdv 3013 abssdv 3014 opprc 3570 dfnfc2 3598 intss 3636 intab 3644 dfiin2g 3690 disjss1 3751 mpteq12dva 3838 el 3931 euotd 3991 reusv1 4190 elirr 4266 sucprcreg 4273 en2lp 4278 tfisi 4310 ssrelrel 4440 issref 4707 iotaval 4878 iota5 4887 iotabidv 4888 funmo 4917 funco 4940 funun 4944 fununi 4967 funcnvuni 4968 funimaexglem 4982 fvssunirng 5190 relfvssunirn 5191 sefvex 5196 nfunsn 5207 f1oresrab 5329 funoprabg 5600 mpt2fvex 5829 1stconst 5842 2ndconst 5843 tfrexlem 5948 rdgexggg 5964 rdgifnon 5966 rdgifnon2 5967 rdgivallem 5968 frectfr 5985 frecrdg 5992 iserd 6132 pitonn 6924 frecuzrdgrrn 9194 frec2uzrdg 9195 frecuzrdgrom 9196 frecuzrdgfn 9198 frecuzrdgsuc 9201 shftfn 9425 2spim 9906 bj-om 10061 bj-nnord 10083 bj-inf2vn 10099 bj-inf2vn2 10100 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |