Home | Metamath
Proof Explorer Theorem List (p. 19 of 466) | < 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: | Metamath Proof Explorer
(1-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mpgbi 1801 | Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
⊢ (∀𝑥𝜑 ↔ 𝜓) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | mpgbir 1802 | Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
⊢ (𝜑 ↔ ∀𝑥𝜓) & ⊢ 𝜓 ⇒ ⊢ 𝜑 | ||
Theorem | nex 1803 | Generalization rule for negated wff. (Contributed by NM, 18-May-1994.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ ∃𝑥𝜑 | ||
Theorem | nfth 1804 | No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfnth 1805 | No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | hbth 1806 |
No variable is (effectively) free in a theorem.
This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form ⊢ (𝜑 → ∀𝑥𝜑) from smaller formulas of this form. These are useful for constructing hypotheses that state "𝑥 is (effectively) not free in 𝜑". (Contributed by NM, 11-May-1993.) This hb* idiom is generally being replaced by the nf* idiom (see nfth 1804), but keeps its interest in some cases. (Revised by BJ, 23-Sep-2022.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | nftru 1807 | The true constant has no free variables. (This can also be proven in one step with nfv 1918, but this proof does not use ax-5 1914.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑥⊤ | ||
Theorem | nffal 1808 | The false constant has no free variables (see nftru 1807). (Contributed by BJ, 6-May-2019.) |
⊢ Ⅎ𝑥⊥ | ||
Theorem | sptruw 1809 | Version of sp 2177 when 𝜑 is true. Instance of a1i 11. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) |
⊢ 𝜑 ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | altru 1810 | For all sets, ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∀𝑥⊤ | ||
Theorem | alfal 1811 | For all sets, ¬ ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.) |
⊢ ∀𝑥 ¬ ⊥ | ||
Axiom | ax-4 1812 | Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1813 for labeling consistency. It should be used only by alim 1813. (Contributed by NM, 21-May-2008.) Use alim 1813 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | alim 1813 | Restatement of Axiom ax-4 1812, for labeling consistency. It should be the only theorem using ax-4 1812. (Contributed by NM, 10-Jan-1993.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | alimi 1814 | Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | 2alimi 1815 | Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) | ||
Theorem | ala1 1816 | Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜑)) | ||
Theorem | al2im 1817 | Closed form of al2imi 1818. Version of alim 1813 for a nested implication. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) | ||
Theorem | al2imi 1818 | Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | alanimi 1819 | Variant of al2imi 1818 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒) | ||
Theorem | alimdh 1820 | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1813. (Contributed by NM, 4-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | albi 1821 | Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | albii 1822 | Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) | ||
Theorem | 2albii 1823 | Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) | ||
Theorem | 3albii 1824 | Inference adding three universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 10-Aug-2018.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥∀𝑦∀𝑧𝜑 ↔ ∀𝑥∀𝑦∀𝑧𝜓) | ||
Theorem | sylgt 1825 | Closed form of sylg 1826. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜓 → 𝜒) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒))) | ||
Theorem | sylg 1826 | A syllogism combined with generalization. Inference associated with sylgt 1825. General form of alrimih 1827. (Contributed by BJ, 4-Oct-2019.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
Theorem | alrimih 1827 | Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21h 2285. Instance of sylg 1826. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | hbxfrbi 1828 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2870 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | alex 1829 | Universal quantifier in terms of existential quantifier and negation. Dual of df-ex 1783. See also the dual pair alnex 1784 / exnal 1830. Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | ||
Theorem | exnal 1830 | Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1784. See also the dual pair df-ex 1783 / alex 1829. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | ||
Theorem | 2nalexn 1831 | Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∀𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦 ¬ 𝜑) | ||
Theorem | 2exnaln 1832 | Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | 2nexaln 1833 | Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | alimex 1834 | An equivalence between an implication with a universally quantified consequent and an implication with an existentially quantified antecedent. An interesting case is when the same formula is substituted for both 𝜑 and 𝜓, since then both implications express a type of nonfreeness. See also eximal 1785. (Contributed by BJ, 12-May-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) ↔ (∃𝑥 ¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | aleximi 1835 | A variant of al2imi 1818: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2149, sps 2179 and eximd 2210, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | alexbii 1836 | Biconditional form of aleximi 1835. (Contributed by BJ, 16-Nov-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exim 1837 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | eximi 1838 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 2eximi 1839 | Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) | ||
Theorem | eximii 1840 | Inference associated with eximi 1838. (Contributed by BJ, 3-Feb-2018.) |
⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
Theorem | exa1 1841 | Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∃𝑥𝜑 → ∃𝑥(𝜓 → 𝜑)) | ||
Theorem | 19.38 1842 | Theorem 19.38 of [Margaris] p. 90. The converse holds under nonfreeness conditions, see 19.38a 1843 and 19.38b 1844. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 2200. (Revised by Wolf Lammen, 2-Jan-2018.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.38a 1843 | Under a nonfreeness hypothesis, the implication 19.38 1842 can be strengthened to an equivalence. See also 19.38b 1844. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.) |
⊢ (Ⅎ𝑥𝜑 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | 19.38b 1844 | Under a nonfreeness hypothesis, the implication 19.38 1842 can be strengthened to an equivalence. See also 19.38a 1843. (Contributed by BJ, 3-Nov-2021.) (Proof shortened by Wolf Lammen, 9-Jul-2022.) |
⊢ (Ⅎ𝑥𝜓 → ((∃𝑥𝜑 → ∀𝑥𝜓) ↔ ∀𝑥(𝜑 → 𝜓))) | ||
Theorem | imnang 1845 | Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥 ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | alinexa 1846 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | exnalimn 1847 | Existential quantification of a conjunction expressed with only primitive symbols (→, ¬, ∀). (Contributed by NM, 10-May-1993.) State the most general instance. (Revised by BJ, 29-Sep-2019.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ¬ ∀𝑥(𝜑 → ¬ 𝜓)) | ||
Theorem | alexn 1848 | A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥∃𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∀𝑦𝜑) | ||
Theorem | 2exnexn 1849 | Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.) |
⊢ (∃𝑥∀𝑦𝜑 ↔ ¬ ∀𝑥∃𝑦 ¬ 𝜑) | ||
Theorem | exbi 1850 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | exbii 1851 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) | ||
Theorem | 2exbii 1852 | Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) | ||
Theorem | 3exbii 1853 | Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) | ||
Theorem | nfbiit 1854 | Equivalence theorem for the nonfreeness predicate. Closed form of nfbii 1855. (Contributed by Giovanni Mascellani, 10-Apr-2018.) Reduce axiom usage. (Revised by BJ, 6-May-2019.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)) | ||
Theorem | nfbii 1855 | Equality theorem for the nonfreeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) | ||
Theorem | nfxfr 1856 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfxfrd 1857 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜒 → Ⅎ𝑥𝜑) | ||
Theorem | nfnbi 1858 | A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 6-Oct-2024.) |
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfnbiOLD 1859 | Obsolete version of nfnbi 1858 as of 6-Oct-2024. (Contributed by BJ, 6-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfnt 1860 | If a variable is nonfree in a proposition, then it is nonfree 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 1787 changed. (Revised by Wolf Lammen, 4-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfn 1861 | Inference associated with nfnt 1860. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1787 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥 ¬ 𝜑 | ||
Theorem | nfnd 1862 | Deduction associated with nfnt 1860. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | ||
Theorem | exanali 1863 | A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.) |
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | 2exanali 1864 | Theorem *11.521 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥∃𝑦(𝜑 ∧ ¬ 𝜓) ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | exancom 1865 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | exan 1866 | 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, 6-Nov-2022.) Expand hypothesis. (Revised by Steven Nguyen, 19-Jun-2023.) |
⊢ ∃𝑥𝜑 & ⊢ 𝜓 ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | alrimdh 1867 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2201 and 19.21h 2285. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdh 1868 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | nexdh 1869 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albidh 1870 | Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidh 1871 | Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exsimpl 1872 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) | ||
Theorem | exsimpr 1873 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓) | ||
Theorem | 19.26 1874 | 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 1875 | Theorem 19.26 1874 with two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.26-3an 1876 | Theorem 19.26 1874 with triple conjunction. (Contributed by NM, 13-Sep-2011.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | 19.29 1877 | Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1878. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r 1878 | Variation of 19.29 1877. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r2 1879 | Variation of 19.29r 1878 with double quantification. (Contributed by NM, 3-Feb-2005.) |
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29x 1880 | Variation of 19.29 1877 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.35 1881 | 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 1882 | Inference associated with 19.35 1881. (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.35ri 1883 | Inference associated with 19.35 1881. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 → ∃𝑥𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | 19.25 1884 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓)) | ||
Theorem | 19.30 1885 | Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43 1886 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43OLD 1887 | Obsolete proof of 19.43 1886. Do not delete as it is referenced on the mmrecent.html 1886 page and in conventions-labels 28774. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.33 1888 | Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | 19.33b 1889 | The antecedent provides a condition implying the converse of 19.33 1888. (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 1890 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.40-2 1891 | 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 1892 | The antecedent provides a condition implying the converse of 19.40 1890. This is to 19.40 1890 what 19.33b 1889 is to 19.33 1888. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | albiim 1893 | Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜑))) | ||
Theorem | 2albiim 1894 | Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) ↔ (∀𝑥∀𝑦(𝜑 → 𝜓) ∧ ∀𝑥∀𝑦(𝜓 → 𝜑))) | ||
Theorem | exintrbi 1895 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | exintr 1896 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) (Proof shortened by BJ, 16-Sep-2022.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | alsyl 1897 | Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒)) | ||
Theorem | nfimd 1898 | If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1900. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1787 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1899. (Revised by Wolf Lammen, 10-Jul-2022.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | nfimt 1899 | Closed form of nfim 1900 and nfimd 1898. (Contributed by BJ, 20-Oct-2021.) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6-Jul-2022.) |
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓)) | ||
Theorem | nfim 1900 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1899. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1787 changed. (Revised by Wolf Lammen, 17-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |