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 1459 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alrimiv.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | alrimih 1398 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1282 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-5 1376 ax-gen 1378 ax-17 1459 |
This theorem is referenced by: alrimivv 1796 nfdv 1798 axext4 2065 eqrdv 2079 abbi2dv 2197 abbi1dv 2198 elex22 2614 elex2 2615 spcimdv 2682 spcimedv 2684 pm13.183 2732 sbcthdv 2829 sbcimdv 2879 ssrdv 3005 ss2abdv 3067 abssdv 3068 opprc 3591 dfnfc2 3619 intss 3657 intab 3665 dfiin2g 3711 disjss1 3772 mpteq12dva 3859 el 3952 euotd 4009 reusv1 4208 elirr 4284 sucprcreg 4292 en2lp 4297 tfisi 4328 ssrelrel 4458 issref 4727 iotaval 4898 iota5 4907 iotabidv 4908 funmo 4937 funco 4960 funun 4964 fununi 4987 funcnvuni 4988 funimaexglem 5002 fvssunirng 5210 relfvssunirn 5211 sefvex 5216 nfunsn 5228 f1oresrab 5350 funoprabg 5620 mpt2fvex 5849 1stconst 5862 2ndconst 5863 tfrexlem 5971 rdgexggg 5987 rdgifnon 5989 rdgifnon2 5990 rdgivallem 5991 frectfr 6008 frecrdg 6015 iserd 6155 pitonn 7016 frecuzrdgrrn 9410 frec2uzrdg 9411 frecuzrdgrom 9412 frecuzrdgfn 9414 frecuzrdgsuc 9417 shftfn 9712 2spim 10577 bj-om 10732 bj-nnord 10753 bj-inf2vn 10769 bj-inf2vn2 10770 bj-findis 10774 |
Copyright terms: Public domain | W3C validator |