![]() |
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 1594 via the use of distinct variable conditions combined with ax-17 1537. 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 2047 derived from df-eu 2045. 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 1537 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.21h 1568 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ial 1545 ax-i5r 1546 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm11.53 1907 cbval2 1933 cbvaldvaw 1942 sbhb 1956 2sb6 2000 sbcom2v 2001 2sb6rf 2006 2exsb 2025 moanim 2116 r3al 2538 ceqsralt 2787 rspc2gv 2876 euind 2947 reu2 2948 reuind 2965 unissb 3865 dfiin2g 3945 tfi 4610 asymref 5043 dff13 5803 mpo2eqb 6020 |
Copyright terms: Public domain | W3C validator |