![]() |
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 2201. (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 2189 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1827 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 |
This theorem is referenced by: sbimd 2238 sbbid 2239 nf5d 2281 axc4i 2316 19.12 2321 nfsbd 2525 mobid 2549 mo3 2563 eubid 2586 2moexv 2628 eupicka 2635 2moex 2641 2mo 2649 abbid 2808 nfcd 2896 nfabdwOLD 2932 ceqsalgALT 3481 ceqsexOLD 3496 vtocldf 3513 rspcdf 3571 elrab3t 3649 morex 3682 sbciedf 3788 csbiebt 3890 csbiedf 3891 ssrd 3954 eqrd 3968 invdisj 5094 zfrepclf 5256 eusv2nf 5355 ssopab2bw 5509 ssopab2b 5511 imadif 6590 eusvobj1 7355 ssoprab2b 7431 eqoprab2bw 7432 ovmpodxf 7510 axrepnd 10537 axunnd 10539 axpownd 10544 axregndlem1 10545 axacndlem1 10550 axacndlem2 10551 axacndlem3 10552 axacndlem4 10553 axacndlem5 10554 axacnd 10555 mreexexd 17535 acsmapd 18450 isch3 30225 ssrelf 31576 eqrelrd2 31577 esumeq12dvaf 32670 bnj1366 33481 bnj571 33558 bnj964 33595 iota5f 34335 bj-hbext 35204 bj-nfext 35206 wl-mo3t 36060 wl-ax11-lem3 36068 cover2 36202 alrimii 36607 mpobi123f 36650 mptbi12f 36654 ss2iundf 42005 pm11.57 42743 pm11.59 42745 tratrb 42892 hbexg 42912 e2ebindALT 43285 mpteq1dfOLD 43536 mpteq12daOLD 43543 dvnmul 44258 stoweidlem34 44349 sge0fodjrnlem 44731 pimrecltpos 45023 pimrecltneg 45039 smfaddlem1 45078 smfresal 45103 smfinflem 45132 smfinfmpt 45134 ichnfim 45730 ovmpordxf 46488 setrec1lem4 47209 |
Copyright terms: Public domain | W3C validator |