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 1563 via the use of distinct variable conditions combined with ax-17 1506. 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 2011 derived from df-eu 2009. 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 1506 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | 1 | 19.21h 1537 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1333 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-gen 1429 ax-4 1490 ax-17 1506 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm11.53 1875 cbval2 1901 sbhb 1920 2sb6 1964 sbcom2v 1965 2sb6rf 1970 2exsb 1989 moanim 2080 r3al 2501 ceqsralt 2739 rspc2gv 2828 euind 2899 reu2 2900 reuind 2917 unissb 3804 dfiin2g 3884 tfi 4543 asymref 4973 dff13 5720 mpo2eqb 5932 |
Copyright terms: Public domain | W3C validator |