Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alrimi | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (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 | nfri 1512 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1462 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1346 Ⅎwnf 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-5 1440 ax-gen 1442 ax-4 1503 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: axc4i 1535 19.32r 1673 cbv3 1735 sbbid 1839 sbalyz 1992 dvelimdf 2009 dvelimor 2011 nf5d 2018 abbid 2287 nfcd 2307 nfabdw 2331 ralrimi 2541 r19.32r 2616 ceqsalg 2758 ceqsex 2768 vtocldf 2781 elrab3t 2885 morex 2914 sbciedf 2990 csbiebt 3088 csbiedf 3089 ssrd 3152 rgenm 3517 invdisj 3983 ssopab2b 4261 eusv2nf 4441 sniota 5189 imadif 5278 funimaexglem 5281 eusvobj1 5840 ssoprab2b 5910 ovmpodxf 5978 |
Copyright terms: Public domain | W3C validator |