![]() |
Metamath
Proof Explorer Theorem List (p. 20 of 431) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28080) |
![]() (28081-29605) |
![]() (29606-43060) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2exnaln 1901 | Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | 2nexaln 1902 | Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | alimex 1903 | A utility theorem. An interesting case is when the same formula is substituted for both 𝜑 and 𝜓, since then both implications express a type of non-freeness. See also eximal 1852. (Contributed by BJ, 12-May-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) ↔ (∃𝑥 ¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | aleximi 1904 | A variant of al2imi 1888: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2173, sps 2198 and eximd 2228, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | alexbii 1905 | Biconditional form of aleximi 1904. (Contributed by BJ, 16-Nov-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exim 1906 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | eximi 1907 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 2eximi 1908 | Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) | ||
Theorem | eximii 1909 | Inference associated with eximi 1907. (Contributed by BJ, 3-Feb-2018.) |
⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
Theorem | exa1 1910 | Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∃𝑥𝜑 → ∃𝑥(𝜓 → 𝜑)) | ||
Theorem | 19.38 1911 | Theorem 19.38 of [Margaris] p. 90. The converse holds under non-freeness conditions, see 19.38a 1912 and 19.38b 1913. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 2216. (Revised by Wolf Lammen, 2-Jan-2018.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.38a 1912 | Under a non-freeness hypothesis, the implication 19.38 1911 can be strengthened to an equivalence. See also 19.38b 1913. (Contributed by BJ, 3-Nov-2021.) |
⊢ (Ⅎ𝑥𝜑 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | 19.38b 1913 | Under a non-freeness hypothesis, the implication 19.38 1911 can be strengthened to an equivalence. See also 19.38a 1912. (Contributed by BJ, 3-Nov-2021.) |
⊢ (Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | imnang 1914 | Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥 ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | alinexa 1915 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | alexn 1916 | A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥∃𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∀𝑦𝜑) | ||
Theorem | 2exnexn 1917 | Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.) |
⊢ (∃𝑥∀𝑦𝜑 ↔ ¬ ∀𝑥∃𝑦 ¬ 𝜑) | ||
Theorem | exbi 1918 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | exbii 1919 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) | ||
Theorem | 2exbii 1920 | Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) | ||
Theorem | 3exbii 1921 | Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) | ||
Theorem | nfbiit 1922 | Equivalence theorem for the non-freeness predicate. Closed form of nfbii 1923. (Contributed by BJ, 6-May-2019.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)) | ||
Theorem | nfbii 1923 | Equality theorem for the non-freeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1855 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) | ||
Theorem | nfxfr 1924 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfxfrd 1925 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜒 → Ⅎ𝑥𝜑) | ||
Theorem | nfnbi 1926 | A variable is non-free in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019.) |
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfnt 1927 | If a variable is non-free in a proposition, then it is non-free in its negation. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) df-nf 1855 changed. (Revised by Wolf Lammen, 4-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfntOLDOLD 1928 | Obsolete proof of nfnt 1927 as of 3-Nov-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) df-nf 1855 changed. (Revised by Wolf Lammen, 4-Oct-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfn 1929 | Inference associated with nfnt 1927. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1855 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥 ¬ 𝜑 | ||
Theorem | nfnd 1930 | Deduction associated with nfnt 1927. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | ||
Theorem | exanali 1931 | A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.) |
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | exancom 1932 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | exan 1933 | Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof shortened by Wolf Lammen, 8-Oct-2021.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | exanOLD 1934 | Obsolete proof of exan 1933 as of 8-Oct-2021. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | alrimdh 1935 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2218 and 19.21h 2264. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdh 1936 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | nexdh 1937 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albidh 1938 | Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidh 1939 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exsimpl 1940 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) | ||
Theorem | exsimpr 1941 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓) | ||
Theorem | 19.40 1942 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.26 1943 | Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.26-2 1944 | Theorem 19.26 1943 with two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.26-3an 1945 | Theorem 19.26 1943 with triple conjunction. (Contributed by NM, 13-Sep-2011.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | 19.29 1946 | Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1947. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r 1947 | Variation of 19.29 1946. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r2 1948 | Variation of 19.29r 1947 with double quantification. (Contributed by NM, 3-Feb-2005.) |
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29x 1949 | Variation of 19.29 1946 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.35 1950 | Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.35i 1951 | Inference associated with 19.35 1950. (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.35ri 1952 | Inference associated with 19.35 1950. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 → ∃𝑥𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | 19.25 1953 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓)) | ||
Theorem | 19.30 1954 | Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43 1955 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43OLD 1956 | Obsolete proof of 19.43 1955. Do not delete as it is referenced on the mmrecent.html page and in conventions-label 27565. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.33 1957 | Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | 19.33b 1958 | The antecedent provides a condition implying the converse of 19.33 1957. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.) |
⊢ (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓))) | ||
Theorem | 19.40-2 1959 | Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with two quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑥∃𝑦𝜓)) | ||
Theorem | 19.40b 1960 | The antecedent provides a condition implying the converse of 19.40 1942. This is to 19.40 1942 what 19.33b 1958 is to 19.33 1957. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | albiim 1961 | Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜑))) | ||
Theorem | 2albiim 1962 | Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) ↔ (∀𝑥∀𝑦(𝜑 → 𝜓) ∧ ∀𝑥∀𝑦(𝜓 → 𝜑))) | ||
Theorem | exintrbi 1963 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | exintr 1964 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | alsyl 1965 | Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒)) | ||
Theorem | nfimt 1966 | Closed form of nfim 1970 and curried (exported) form of nfimt2 1967. (Contributed by BJ, 20-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → (Ⅎ𝑥𝜓 → Ⅎ𝑥(𝜑 → 𝜓))) | ||
Theorem | nfimt2 1967 | Closed form of nfim 1970 and uncurried (imported) form of nfimt 1966. (Contributed by BJ, 20-Oct-2021.) |
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓)) | ||
Theorem | nfimd 1968 | If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 → 𝜒). Deduction form of nfimt 1966. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1855 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | nfimdOLDOLD 1969 | Obsolete proof of nfimd 1968 as of 3-Nov-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1855 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | nfim 1970 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1966. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1855 changed. (Revised by Wolf Lammen, 17-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 → 𝜓) | ||
Theorem | nfand 1971 | If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | nf3and 1972 | Deduction form of bound-variable hypothesis builder nf3an 1976. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝜃) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | nfan 1973 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | ||
Theorem | nfanOLD 1974 | Obsolete proof of nfan 1973 as of 9-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | ||
Theorem | nfnan 1975 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ⊼ 𝜓). (Contributed by Scott Fenton, 2-Jan-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ⊼ 𝜓) | ||
Theorem | nf3an 1976 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) | ||
Theorem | nfbid 1977 | If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 ↔ 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | nfbi 1978 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) | ||
Theorem | nfor 1979 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∨ 𝜓). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) | ||
Theorem | nf3or 1980 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∨ 𝜓 ∨ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Theorem | nfbiiOLD 1981 | Obsolete proof of nfbii 1923 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) | ||
Theorem | nfxfrOLD 1982 | Obsolete proof of nfxfr 1924 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfxfrdOLD 1983 | Obsolete proof of nfxfrd 1925 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜒 → Ⅎ𝑥𝜑) | ||
Axiom | ax-5 1984* |
Axiom of Distinctness. This axiom quantifies a variable over a formula
in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of [Monk2] p. 113.
(See comments in ax5ALT 34692 about the logical redundancy of ax-5 1984 in the presence of our obsolete axioms.) This axiom essentially says that if 𝑥 does not occur in 𝜑, i.e. 𝜑 does not depend on 𝑥 in any way, then we can add the quantifier ∀𝑥 to 𝜑 with no further assumptions. By sp 2196, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | ax5d 1985* | ax-5 1984 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders. (Contributed by NM, 1-Mar-2013.) |
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | ax5e 1986* | A rephrasing of ax-5 1984 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.) |
⊢ (∃𝑥𝜑 → 𝜑) | ||
Theorem | ax5ea 1987* | If a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable. (Contributed by BJ, 28-Dec-2020.) |
⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | nfv 1988* | If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Definition change. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfvd 1989* | nfv 1988 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1968. (Contributed by Mario Carneiro, 6-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | alimdv 1990* | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1883. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdv 1991* | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1906. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | 2alimdv 1992* | Deduction form of Theorem 19.20 of [Margaris] p. 90 with two quantifiers, see alim 1883. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2eximdv 1993* | Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1906. (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) | ||
Theorem | albidv 1994* | Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidv 1995* | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | 2albidv 1996* | Formula-building rule for two universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2exbidv 1997* | Formula-building rule for two existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) | ||
Theorem | 3exbidv 1998* | Formula-building rule for three existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧𝜓 ↔ ∃𝑥∃𝑦∃𝑧𝜒)) | ||
Theorem | 4exbidv 1999* | Formula-building rule for four existential quantifiers (deduction rule). (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) | ||
Theorem | alrimiv 2000* | Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2218 and 19.21v 2013. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |