| 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 1542 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
| 3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
| 4 | 2, 3 | alrimih 1492 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∀wal 1371 Ⅎwnf 1483 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1470 ax-gen 1472 ax-4 1533 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 |
| This theorem is referenced by: axc4i 1565 19.32r 1703 cbv3 1765 sbbid 1869 sbalyz 2027 dvelimdf 2044 dvelimor 2046 nf5d 2053 abbid 2322 nfcd 2343 nfabdw 2367 ralrimi 2577 r19.32r 2652 ceqsalg 2800 ceqsex 2810 vtocldf 2824 elrab3t 2928 morex 2957 sbciedf 3034 csbiebt 3133 csbiedf 3134 ssrd 3198 invdisj 4038 ssopab2b 4323 eusv2nf 4503 sniota 5262 imadif 5354 funimaexglem 5357 eusvobj1 5931 ssoprab2b 6002 ovmpodxf 6071 nninfinf 10588 |
| Copyright terms: Public domain | W3C validator |