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 2207. (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 2195 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1824 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-ex 1781 df-nf 1785 |
This theorem is referenced by: sbimd 2245 sbbid 2246 nf5d 2292 axc4i 2341 19.12 2346 cbv2OLD 2427 nfsbd 2564 mobid 2634 mo3 2648 eubid 2673 2moexv 2712 eupicka 2719 2moex 2725 2mo 2733 abbid 2887 nfcd 2968 nfabdw 3000 ceqsalgALT 3530 ceqsex 3540 vtocldf 3555 rspcdf 3610 elrab3t 3679 morex 3710 sbciedf 3813 csbiebt 3912 csbiedf 3913 ssrd 3972 eqrd 3986 invdisj 5050 zfrepclf 5198 eusv2nf 5296 ssopab2bw 5434 ssopab2b 5436 imadif 6438 eusvobj1 7150 ssoprab2b 7223 eqoprab2bw 7224 ovmpodxf 7300 axrepnd 10016 axunnd 10018 axpownd 10023 axregndlem1 10024 axacndlem1 10029 axacndlem2 10030 axacndlem3 10031 axacndlem4 10032 axacndlem5 10033 axacnd 10034 mreexexd 16919 acsmapd 17788 isch3 29018 ssrelf 30366 eqrelrd2 30367 esumeq12dvaf 31290 bnj1366 32101 bnj571 32178 bnj964 32215 iota5f 32955 bj-hbext 34044 bj-nfext 34046 wl-mo3t 34827 wl-ax11-lem3 34834 cover2 35004 alrimii 35412 mpobi123f 35455 mptbi12f 35459 ss2iundf 40053 pm11.57 40770 pm11.59 40772 tratrb 40919 hbexg 40939 e2ebindALT 41312 mpteq1df 41555 mpteq12da 41562 dvnmul 42277 stoweidlem34 42368 sge0fodjrnlem 42747 pimrecltpos 43036 pimrecltneg 43050 smfaddlem1 43088 smfresal 43112 smfsupmpt 43138 smfinflem 43140 smfinfmpt 43142 dfich2OLD 43665 ichnfim 43673 ovmpordxf 44436 setrec1lem4 44842 |
Copyright terms: Public domain | W3C validator |