| 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 1541 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
| 3 | alrimi.2 | . 2 ⊢ (𝜑 → 𝜓) | |
| 4 | 2, 3 | alrimih 1491 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∀wal 1370 Ⅎwnf 1482 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-5 1469 ax-gen 1471 ax-4 1532 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 |
| This theorem is referenced by: axc4i 1564 19.32r 1702 cbv3 1764 sbbid 1868 sbalyz 2026 dvelimdf 2043 dvelimor 2045 nf5d 2052 abbid 2321 nfcd 2342 nfabdw 2366 ralrimi 2576 r19.32r 2651 ceqsalg 2799 ceqsex 2809 vtocldf 2823 elrab3t 2927 morex 2956 sbciedf 3033 csbiebt 3132 csbiedf 3133 ssrd 3197 invdisj 4037 ssopab2b 4322 eusv2nf 4502 sniota 5261 imadif 5353 funimaexglem 5356 eusvobj1 5930 ssoprab2b 6001 ovmpodxf 6070 nninfinf 10586 |
| Copyright terms: Public domain | W3C validator |