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 1499 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | alrimih 1449 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1333 Ⅎwnf 1440 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-5 1427 ax-gen 1429 ax-4 1490 |
This theorem depends on definitions: df-bi 116 df-nf 1441 |
This theorem is referenced by: axc4i 1522 19.32r 1660 cbv3 1722 sbbid 1826 sbalyz 1979 dvelimdf 1996 dvelimor 1998 nf5d 2005 abbid 2274 nfcd 2294 nfabdw 2318 ralrimi 2528 r19.32r 2603 ceqsalg 2740 ceqsex 2750 vtocldf 2763 elrab3t 2867 morex 2896 sbciedf 2972 csbiebt 3070 csbiedf 3071 ssrd 3133 rgenm 3496 invdisj 3959 ssopab2b 4236 eusv2nf 4416 sniota 5162 imadif 5250 funimaexglem 5253 eusvobj1 5811 ssoprab2b 5878 ovmpodxf 5946 |
Copyright terms: Public domain | W3C validator |