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 2198. (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 2185 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1815 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: sbimd 2236 sbbid 2237 nf5d 2284 axc4i 2333 19.12 2338 cbv2OLD 2421 nfsbd 2560 mobid 2630 mo3 2644 eubid 2669 2moexv 2708 eupicka 2715 2moex 2721 2mo 2729 axbndOLD 2792 abbid 2887 nfcd 2968 nfabdw 3000 ceqsalgALT 3531 ceqsex 3541 vtocldf 3556 rspcdf 3609 elrab3t 3678 morex 3709 sbciedf 3812 csbiebt 3911 csbiedf 3912 ssrd 3971 eqrd 3985 invdisj 5042 zfrepclf 5190 eusv2nf 5287 ssopab2bw 5426 ssopab2b 5428 imadif 6432 eusvobj1 7139 ssoprab2b 7212 eqoprab2bw 7213 ovmpodxf 7289 axrepnd 10005 axunnd 10007 axpownd 10012 axregndlem1 10013 axacndlem1 10018 axacndlem2 10019 axacndlem3 10020 axacndlem4 10021 axacndlem5 10022 axacnd 10023 mreexexd 16909 acsmapd 17778 isch3 28946 ssrelf 30295 eqrelrd2 30296 esumeq12dvaf 31190 bnj1366 32001 bnj571 32078 bnj964 32115 iota5f 32853 bj-hbext 33942 bj-nfext 33944 wl-mo3t 34694 wl-ax11-lem3 34701 cover2 34872 alrimii 35280 mpobi123f 35323 mptbi12f 35327 ss2iundf 39884 pm11.57 40601 pm11.59 40603 tratrb 40750 hbexg 40770 e2ebindALT 41143 mpteq1df 41386 mpteq12da 41393 dvnmul 42108 stoweidlem34 42200 sge0fodjrnlem 42579 pimrecltpos 42868 pimrecltneg 42882 smfaddlem1 42920 smfresal 42944 smfsupmpt 42970 smfinflem 42972 smfinfmpt 42974 dfich2OLD 43463 ichnfim 43471 ovmpordxf 44285 setrec1lem4 44691 |
Copyright terms: Public domain | W3C validator |