![]() |
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 1519 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1469 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 Ⅎwnf 1460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1447 ax-gen 1449 ax-4 1510 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: axc4i 1542 19.32r 1680 cbv3 1742 sbbid 1846 sbalyz 1999 dvelimdf 2016 dvelimor 2018 nf5d 2025 abbid 2294 nfcd 2314 nfabdw 2338 ralrimi 2548 r19.32r 2623 ceqsalg 2765 ceqsex 2775 vtocldf 2788 elrab3t 2892 morex 2921 sbciedf 2998 csbiebt 3096 csbiedf 3097 ssrd 3160 rgenm 3525 invdisj 3997 ssopab2b 4276 eusv2nf 4456 sniota 5207 imadif 5296 funimaexglem 5299 eusvobj1 5861 ssoprab2b 5931 ovmpodxf 5999 |
Copyright terms: Public domain | W3C validator |