Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.21v | GIF version |
Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (𝜑 → ∀𝑥𝜑) in 19.21 1576 via the use of distinct variable conditions combined with ax-17 1519. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g., euf 2024 derived from df-eu 2022. The "f" stands for "not free in" which is less restrictive than "does not occur in". (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
19.21v | ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1519 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.21h 1550 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm11.53 1888 cbval2 1914 sbhb 1933 2sb6 1977 sbcom2v 1978 2sb6rf 1983 2exsb 2002 moanim 2093 r3al 2514 ceqsralt 2757 rspc2gv 2846 euind 2917 reu2 2918 reuind 2935 unissb 3826 dfiin2g 3906 tfi 4566 asymref 4996 dff13 5747 mpo2eqb 5962 |
Copyright terms: Public domain | W3C validator |