Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 19.21v | Unicode 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 1547 via the use of distinct variable conditions combined with ax-17 1491. 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 1982 derived from df-eu 1980. 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 1491 | . 2 | |
2 | 1 | 19.21h 1521 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1314 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm11.53 1851 cbval2 1873 sbhb 1893 2sb6 1937 sbcom2v 1938 2sb6rf 1943 2exsb 1962 moanim 2051 r3al 2454 ceqsralt 2687 rspc2gv 2775 euind 2844 reu2 2845 reuind 2862 unissb 3736 dfiin2g 3816 tfi 4466 asymref 4894 dff13 5637 mpo2eqb 5848 |
Copyright terms: Public domain | W3C validator |