![]() |
Metamath
Proof Explorer Theorem List (p. 32 of 486) | < 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-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | r19.26 3101 | Restricted quantifier version of 19.26 1866. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.26-3 3102 | Version of r19.26 3101 with three quantifiers. (Contributed by FL, 22-Nov-2010.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓 ∧ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralbiim 3103 | Split a biconditional and distribute quantifier. Restricted quantifier version of albiim 1885. (Contributed by NM, 3-Jun-2012.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑))) | ||
Theorem | r19.29 3104 | Restricted quantifier version of 19.29 1869. See also r19.29r 3106. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 22-Dec-2024.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29OLD 3105 | Obsolete version of r19.29 3104 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29r 3106 | Restricted quantifier version of 19.29r 1870; variation of r19.29 3104. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29rOLD 3107 | Obsolete version of r19.29r 3106 as of 22-Dec-2024. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29imd 3108 | Theorem 19.29 of [Margaris] p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜒)) | ||
Theorem | r19.40 3109 | Restricted quantifier version of Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.30 3110 | Restricted quantifier version of 19.30 1877. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 5-Nov-2024.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.30OLD 3111 | Obsolete version of 19.30 1877 as of 5-Nov-2024. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.43 3112 | Restricted quantifier version of 19.43 1878. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | 2ralimi 3113 | Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | 3ralimi 3114 | Inference quantifying both antecedent and consequent three times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | 4ralimi 3115 | Inference quantifying both antecedent and consequent four times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓) | ||
Theorem | 5ralimi 3116 | Inference quantifying both antecedent and consequent five times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 𝜓) | ||
Theorem | 6ralimi 3117 | Inference quantifying both antecedent and consequent six times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑡 ∈ 𝐸 ∀𝑢 ∈ 𝐹 𝜓) | ||
Theorem | 2ralbii 3118 | Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | 2rexbii 3119 | Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | ||
Theorem | 3ralbii 3120 | Inference adding three restricted universal quantifiers to both sides of an equivalence. (Contributed by Peter Mazsa, 25-Jul-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | 4ralbii 3121 | Inference adding four restricted universal quantifiers to both sides of an equivalence. (Contributed by Scott Fenton, 28-Feb-2025.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓) | ||
Theorem | 2ralbiim 3122 | Split a biconditional and distribute two restricted universal quantifiers, analogous to 2albiim 1886 and ralbiim 3103. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ↔ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜓 → 𝜑))) | ||
Theorem | ralnex2 3123 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) | ||
Theorem | ralnex3 3124 | Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝜑) | ||
Theorem | rexnal2 3125 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | ||
Theorem | rexnal3 3126 | Relationship between three restricted universal and existential quantifiers. (Contributed by Thierry Arnoux, 12-Jul-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑) | ||
Theorem | nrexralim 3127 | Negation of a complex predicate calculus formula. (Contributed by FL, 31-Jul-2009.) |
⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝜓) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | r19.26-2 3128 | Restricted quantifier version of 19.26-2 1867. Version of r19.26 3101 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | ||
Theorem | 2r19.29 3129 | Theorem r19.29 3104 with two quantifiers. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.29d2r 3130 | Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) | ||
Theorem | r19.29d2rOLD 3131 | Obsolete version of r19.29d2r 3130 as of 4-Nov-2024. (Contributed by Thierry Arnoux, 30-Jan-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜓 ∧ 𝜒)) | ||
Theorem | r2allem 3132 | Lemma factoring out common proof steps of r2alf 3269 and r2al 3185. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 9-Jan-2020.) |
⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑))) ⇒ ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | ||
Theorem | r2exlem 3133 | Lemma factoring out common proof steps in r2exf 3270 an r2ex 3186. Introduced to reduce dependencies on axioms. (Contributed by Wolf Lammen, 10-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ¬ 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ¬ 𝜑)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | hbralrimi 3134 | Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3245 and ralrimiv 3135. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimiv 3135* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimiva 3136* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rexlimiva 3137* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimiv 3138* | Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | nrexdv 3139* | Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) | ||
Theorem | ralrimivw 3140* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) | ||
Theorem | rexlimivw 3141* | Weaker version of rexlimiv 3138. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | ralrimdv 3142* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.) |
⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexlimdv 3143* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | ralrimdva 3144* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexlimdva 3145* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdvaa 3146* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdva2 3147* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | r19.29an 3148* | A commonly used pattern in the spirit of r19.29 3104. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒) | ||
Theorem | rexlimdv3a 3149* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3143. (Contributed by NM, 7-Jun-2015.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimdvw 3150* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) | ||
Theorem | rexlimddv 3151* | Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | r19.29a 3152* | A commonly used pattern in the spirit of r19.29 3104. (Contributed by Thierry Arnoux, 22-Nov-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | ralimdv2 3153* | Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | reximdv2 3154* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | reximdvai 3155* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdvaiOLD 3156* | Obsolete version of reximdvai 3155 as of 3-Nov-2024. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimdva 3157* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdva 3158* | Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralimdv 3159* | Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1805). (Contributed by NM, 8-Oct-2003.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximdv 3160* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | reximddv 3161* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | reximddv3 3162* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒) & ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | reximssdv 3163* | Derivation of a restricted existential quantification over a subset (the second hypothesis implies 𝐴 ⊆ 𝐵), deduction form. (Contributed by AV, 21-Aug-2022.) |
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝑥 ∈ 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝜓)) → 𝜒) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) | ||
Theorem | ralbidv2 3164* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | rexbidv2 3165* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) | ||
Theorem | ralbidva 3166* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 29-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidva 3167* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Dec-2019.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | ralbidv 3168* | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | rexbidv 3169* | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 6-Dec-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) | ||
Theorem | r19.21v 3170* | Restricted quantifier version of 19.21v 1935. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.21vOLD 3171* | Obsolete version of r19.21v 3170 as of 11-Dec-2024. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.37v 3172* | Restricted quantifier version of one direction of 19.37v 1988. (The other direction holds iff 𝐴 is nonempty, see r19.37zv 4496.) (Contributed by NM, 2-Apr-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Jun-2023.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.23v 3173* | Restricted quantifier version of 19.23v 1938. Version of r19.23 3244 with a disjoint variable condition. (Contributed by NM, 31-Aug-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | r19.36v 3174* | Restricted quantifier version of one direction of 19.36 2219. (The other direction holds iff 𝐴 is nonempty, see r19.36zv 4501.) (Contributed by NM, 22-Oct-2003.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)) | ||
Theorem | rexlimivOLD 3175* | Obsolete version of rexlimiv 3138 as of 19-Dec-2024.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimivaOLD 3176* | Obsolete version of rexlimiva 3137 as of 23-Dec-2024. (Contributed by NM, 18-Dec-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | rexlimivwOLD 3177* | Obsolete version of rexlimivw 3141 as of 23-Dec-2024. (Contributed by FL, 19-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) | ||
Theorem | r19.27v 3178* | Restricted quantitifer version of one direction of 19.27 2216. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.27zv 4500.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.41v 3179* | Restricted quantifier version 19.41v 1946. Version of r19.41 3251 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) | ||
Theorem | r19.28v 3180* | Restricted quantifier version of one direction of 19.28 2217. (Assuming Ⅎ𝑥𝐴, the other direction holds when 𝐴 is nonempty, see r19.28zv 4495.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) | ||
Theorem | r19.42v 3181* | Restricted quantifier version of 19.42v 1950 (see also 19.42 2225). (Contributed by NM, 27-May-1998.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.32v 3182* | Restricted quantifier version of 19.32v 1936. (Contributed by NM, 25-Nov-2003.) |
⊢ (∀𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.45v 3183* | Restricted quantifier version of one direction of 19.45 2227. The other direction holds when 𝐴 is nonempty, see r19.45zv 4497. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) | ||
Theorem | r19.44v 3184* | One direction of a restricted quantifier version of 19.44 2226. The other direction holds when 𝐴 is nonempty, see r19.44zv 4498. (Contributed by NM, 2-Apr-2004.) |
⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 ∨ 𝜓)) | ||
Theorem | r2al 3185* | Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑)) | ||
Theorem | r2ex 3186* | Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 10-Jan-2020.) |
⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)) | ||
Theorem | r3al 3187* | Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.) (Proof shortened by Wolf Lammen, 30-Dec-2019.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑)) | ||
Theorem | rgen2 3188* | Generalization rule for restricted quantification, with two quantifiers. This theorem should be used in place of rgen2a 3355 since it depends on a smaller set of axioms. (Contributed by NM, 30-May-1999.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 | ||
Theorem | ralrimivv 3189* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜓)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | rexlimivv 3190* | Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓)) ⇒ ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓) | ||
Theorem | ralrimivva 3191* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓) | ||
Theorem | ralrimdvv 3192* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.) |
⊢ (𝜑 → (𝜓 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | rgen3 3193* | Generalization rule for restricted quantification, with three quantifiers. (Contributed by NM, 12-Jan-2008.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝜑) ⇒ ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 | ||
Theorem | ralrimivvva 3194* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶)) → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜓) | ||
Theorem | ralimdvva 3195* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1805). (Contributed by AV, 27-Nov-2019.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | reximdvva 3196* | Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by AV, 5-Jan-2022.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralimdvv 3197* | Deduction doubly quantifying both antecedent and consequent. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) | ||
Theorem | ralimd4v 3198* | Deduction quadrupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 2-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 𝜒)) | ||
Theorem | ralimd6v 3199* | Deduction sextupally quantifying both antecedent and consequent. (Contributed by Scott Fenton, 5-Mar-2025.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐷 ∀𝑝 ∈ 𝐸 ∀𝑞 ∈ 𝐹 𝜒)) | ||
Theorem | ralrimdvva 3200* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |