|   | 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 2206. (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 2194 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | 
| 3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
| 4 | 2, 3 | alrimih 1823 | 1 ⊢ (𝜑 → ∀𝑥𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: sbalex 2241 sbimd 2244 sbbid 2245 nf5d 2283 axc4i 2321 19.12 2326 nfsbd 2526 mobid 2549 mo3 2563 eubid 2586 2moexv 2626 eupicka 2633 2moex 2639 2mo 2647 abbid 2809 nfcd 2897 ceqsalgALT 3517 ceqsexOLD 3530 vtocldf 3559 rspcdf 3608 elrab3t 3690 morex 3724 sbciedf 3830 csbiebt 3927 csbiedf 3928 ssrd 3987 eqrd 4002 invdisj 5128 zfrepclf 5290 eusv2nf 5394 ssopab2bw 5551 ssopab2b 5553 imadif 6649 eusvobj1 7425 ssoprab2b 7503 eqoprab2bw 7504 ovmpodxf 7584 axrepnd 10635 axunnd 10637 axpownd 10642 axregndlem1 10643 axacndlem1 10648 axacndlem2 10649 axacndlem3 10650 axacndlem4 10651 axacndlem5 10652 axacnd 10653 mreexexd 17692 acsmapd 18600 isch3 31261 ssrelf 32628 eqrelrd2 32629 esumeq12dvaf 34033 bnj1366 34844 bnj571 34921 bnj964 34958 iota5f 35725 bj-hbext 36712 bj-nfext 36714 wl-mo3t 37578 wl-ax11-lem3 37589 cover2 37723 alrimii 38127 mpobi123f 38170 mptbi12f 38174 ss2iundf 43677 pm11.57 44413 pm11.59 44415 tratrb 44561 hbexg 44581 e2ebindALT 44954 modelaxreplem2 45001 mpteq1dfOLD 45247 mpteq12daOLD 45254 dvnmul 45963 stoweidlem34 46054 sge0fodjrnlem 46436 pimrecltpos 46728 pimrecltneg 46744 smfaddlem1 46783 smfresal 46808 smfinflem 46837 ichnfim 47456 ovmpordxf 48260 setrec1lem4 49264 | 
| Copyright terms: Public domain | W3C validator |