![]() |
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 1520 via the use of distinct variable conditions combined with ax-17 1464. 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 1953 derived from df-eu 1951. 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 1464 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.21h 1494 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∀wal 1287 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 ax-ial 1472 ax-i5r 1473 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm11.53 1823 cbval2 1844 sbhb 1864 2sb6 1908 sbcom2v 1909 2sb6rf 1914 2exsb 1933 moanim 2022 r3al 2420 ceqsralt 2646 rspc2gv 2733 euind 2802 reu2 2803 reuind 2820 unissb 3683 dfiin2g 3763 tfi 4397 asymref 4817 dff13 5547 mpt22eqb 5754 |
Copyright terms: Public domain | W3C validator |