![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alrimi | Structured version Visualization version GIF version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2222. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
alrimi.1 | ⊢ Ⅎ𝑥𝜑 |
alrimi.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimi | ⊢ (𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimi.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nf5ri 2212 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1900 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1630 Ⅎwnf 1857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-12 2196 |
This theorem depends on definitions: df-bi 197 df-ex 1854 df-nf 1859 |
This theorem is referenced by: nf5d 2265 axc4i 2278 19.12 2309 nfaldOLD 2311 cbv3v 2317 cbv3 2410 cbv2 2415 sbbid 2540 nfsbd 2579 mo3 2645 eupicka 2675 2moex 2681 2mo 2689 axbnd 2739 abbid 2878 nfcd 2897 ceqsalgALT 3371 ceqsex 3381 vtocldf 3396 elrab3t 3503 morex 3531 sbciedf 3612 csbiebt 3694 csbiedf 3695 ssrd 3749 eqrd 3763 invdisj 4790 zfrepclf 4929 eusv2nf 5013 ssopab2b 5152 imadif 6134 eusvobj1 6807 ssoprab2b 6877 ovmpt2dxf 6951 axrepnd 9608 axunnd 9610 axpownd 9615 axregndlem1 9616 axacndlem1 9621 axacndlem2 9622 axacndlem3 9623 axacndlem4 9624 axacndlem5 9625 axacnd 9626 mreexexd 16510 acsmapd 17379 isch3 28407 ssrelf 29734 eqrelrd2 29735 esumeq12dvaf 30402 bnj1366 31207 bnj571 31283 bnj964 31320 iota5f 31913 bj-hbext 33007 bj-nfext 33009 bj-cbv3v2 33033 bj-abbid 33084 wl-mo3t 33671 wl-ax11-lem3 33677 cover2 33821 alrimii 34237 mpt2bi123f 34284 mptbi12f 34288 ss2iundf 38453 pm11.57 39091 pm11.59 39093 tratrb 39248 hbexg 39274 e2ebindALT 39664 mpteq1df 39942 mpteq12da 39951 dvnmul 40661 stoweidlem34 40754 sge0fodjrnlem 41136 preimagelt 41418 preimalegt 41419 pimrecltpos 41425 pimrecltneg 41439 smfaddlem1 41477 smfresal 41501 smfsupmpt 41527 smfinflem 41529 smfinfmpt 41531 ovmpt2rdxf 42627 rspcdf 42934 setrec1lem4 42947 |
Copyright terms: Public domain | W3C validator |