P. 27 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2601-2700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rsp2e 2601	Restricted specialization. (Contributed by FL, 4-Jun-2012.)
|- ( ( x e. A /\ y e. B /\ ph ) -> E. x e. A E. y e. B ph )
Theorem	rspec 2602	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A. x e. A ph   =>    |- ( x e. A -> ph )
Theorem	rgen 2603	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- ( x e. A -> ph )   =>    |- A. x e. A ph
Theorem	rgen2a 2604*	Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2077. Usage of rgen2 2636 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage is discouraged.)
|- ( ( x e. A /\ y e. A ) -> ph )   =>    |- A. x e. A A. y e. A ph
Theorem	rgenw 2605	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A ph
Theorem	rgen2w 2606	Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A A. y e. B ph
Theorem	mprg 2607	Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
|- ( A. x e. A ph -> ps )   &    |- ( x e. A -> ph )   =>    |- ps
Theorem	mprgbir 2608	Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
|- ( ph <-> A. x e. A ps )   &    |- ( x e. A -> ps )   =>    |- ph
Theorem	ralim 2609	Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.)
|- ( A. x e. A ( ph -> ps ) -> ( A. x e. A ph -> A. x e. A ps ) )
Theorem	ralimi2 2610	Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.)
|- ( ( x e. A -> ph ) -> ( x e. B -> ps ) )   =>    |- ( A. x e. A ph -> A. x e. B ps )
Theorem	ralimia 2611	Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- ( A. x e. A ph -> A. x e. A ps )
Theorem	ralimiaa 2612	Inference quantifying both antecedent and consequent. (Contributed by NM, 4-Aug-2007.)
|- ( ( x e. A /\ ph ) -> ps )   =>    |- ( A. x e. A ph -> A. x e. A ps )
Theorem	ralimi 2613	Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
|- ( ph -> ps )   =>    |- ( A. x e. A ph -> A. x e. A ps )
Theorem	2ralimi 2614	Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
|- ( ph -> ps )   =>    |- ( A. x e. A A. y e. B ph -> A. x e. A A. y e. B ps )
Theorem	ral2imi 2615	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ch ) )
Theorem	ralimdaa 2616	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )
Theorem	ralimdva 2617*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )
Theorem	ralimdv 2618*	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )
Theorem	ralimdvva 2619*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1510). (Contributed by AV, 27-Nov-2019.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x e. A A. y e. B ps -> A. x e. A A. y e. B ch ) )
Theorem	ralimdv2 2620*	Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.)
|- ( ph -> ( ( x e. A -> ps ) -> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps -> A. x e. B ch ) )
Theorem	ralrimi 2621	Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
|- F/ x ph   &    |- ( ph -> ( x e. A -> ps ) )   =>    |- ( ph -> A. x e. A ps )
Theorem	ralrimiv 2622*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
|- ( ph -> ( x e. A -> ps ) )   =>    |- ( ph -> A. x e. A ps )
Theorem	ralrimiva 2623*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
|- ( ( ph /\ x e. A ) -> ps )   =>    |- ( ph -> A. x e. A ps )
Theorem	ralrimivw 2624*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
|- ( ph -> ps )   =>    |- ( ph -> A. x e. A ps )
Theorem	r19.21t 2625	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version). (Contributed by NM, 1-Mar-2008.)
|- ( F/ x ph -> ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) ) )
Theorem	r19.21 2626	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by Scott Fenton, 30-Mar-2011.)
|- F/ x ph   =>    |- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )
Theorem	r19.21v 2627*	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A. x e. A ( ph -> ps ) <-> ( ph -> A. x e. A ps ) )
Theorem	ralrimd 2628	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 16-Feb-2004.)
|- F/ x ph   &    |- F/ x ps   &    |- ( ph -> ( ps -> ( x e. A -> ch ) ) )   =>    |- ( ph -> ( ps -> A. x e. A ch ) )
Theorem	ralrimdv 2629*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.)
|- ( ph -> ( ps -> ( x e. A -> ch ) ) )   =>    |- ( ph -> ( ps -> A. x e. A ch ) )
Theorem	ralrimdva 2630*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x e. A ch ) )
Theorem	ralrimivv 2631*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
|- ( ph -> ( ( x e. A /\ y e. B ) -> ps ) )   =>    |- ( ph -> A. x e. A A. y e. B ps )
Theorem	ralrimivva 2632*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ps )   =>    |- ( ph -> A. x e. A A. y e. B ps )
Theorem	ralrimivvva 2633*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014.)
|- ( ( ph /\ ( x e. A /\ y e. B /\ z e. C ) ) -> ps )   =>    |- ( ph -> A. x e. A A. y e. B A. z e. C ps )
Theorem	ralrimdvv 2634*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 1-Jun-2005.)
|- ( ph -> ( ps -> ( ( x e. A /\ y e. B ) -> ch ) ) )   =>    |- ( ph -> ( ps -> A. x e. A A. y e. B ch ) )
Theorem	ralrimdvva 2635*	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 2-Feb-2008.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x e. A A. y e. B ch ) )
Theorem	rgen2 2636*	Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.)
|- ( ( x e. A /\ y e. B ) -> ph )   =>    |- A. x e. A A. y e. B ph
Theorem	rgen3 2637*	Generalization rule for restricted quantification. (Contributed by NM, 12-Jan-2008.)
|- ( ( x e. A /\ y e. B /\ z e. C ) -> ph )   =>    |- A. x e. A A. y e. B A. z e. C ph
Theorem	r19.21bi 2638	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
|- ( ph -> A. x e. A ps )   =>    |- ( ( ph /\ x e. A ) -> ps )
Theorem	rspec2 2639	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
|- A. x e. A A. y e. B ph   =>    |- ( ( x e. A /\ y e. B ) -> ph )
Theorem	rspec3 2640	Specialization rule for restricted quantification. (Contributed by NM, 20-Nov-1994.)
|- A. x e. A A. y e. B A. z e. C ph   =>    |- ( ( x e. A /\ y e. B /\ z e. C ) -> ph )
Theorem	r19.21be 2641	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 21-Nov-1994.)
|- ( ph -> A. x e. A ps )   =>    |- A. x e. A ( ph -> ps )
Theorem	nrex 2642	Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
|- ( x e. A -> -. ps )   =>    |- -. E. x e. A ps
Theorem	nrexdv 2643*	Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
|- ( ( ph /\ x e. A ) -> -. ps )   =>    |- ( ph -> -. E. x e. A ps )
Theorem	rexim 2644	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )
Theorem	reximia 2645	Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> E. x e. A ps )
Theorem	reximi2 2646	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
|- ( ( x e. A /\ ph ) -> ( x e. B /\ ps ) )   =>    |- ( E. x e. A ph -> E. x e. B ps )
Theorem	reximi 2647	Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> E. x e. A ps )
Theorem	reximdai 2648	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
|- F/ x ph   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximdv2 2649*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )
Theorem	reximdvai 2650*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.)
|- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximdv 2651*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximdva 2652*	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )
Theorem	reximddv 2653*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> E. x e. A ch )
Theorem	reximssdv 2654*	Derivation of a restricted existential quantification over a subset (the second hypothesis implies A C_ B), deduction form. (Contributed by AV, 21-Aug-2022.)
|- ( ph -> E. x e. B ps )   &    |- ( ( ph /\ ( x e. B /\ ps ) ) -> x e. A )   &    |- ( ( ph /\ ( x e. B /\ ps ) ) -> ch )   =>    |- ( ph -> E. x e. A ch )
Theorem	reximddv2 2655*	Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)
|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> E. x e. A E. y e. B ch )
Theorem	rexanaliim 2656	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.)
|- ( E. x e. A ( ph /\ -. ps ) -> -. A. x e. A ( ph -> ps ) )
Theorem	r19.12 2657*	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( E. x e. A A. y e. B ph -> A. y e. B E. x e. A ph )
Theorem	r19.23t 2658	Closed theorem form of r19.23 2659. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
|- ( F/ x ps -> ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) ) )
Theorem	r19.23 2659	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 22-Oct-2010.) (Proof shortened by Mario Carneiro, 8-Oct-2016.)
|- F/ x ps   =>    |- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
Theorem	r19.23v 2660*	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
|- ( A. x e. A ( ph -> ps ) <-> ( E. x e. A ph -> ps ) )
Theorem	rexlimi 2661	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- F/ x ps   &    |- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimiv 2662*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
|- ( x e. A -> ( ph -> ps ) )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimiva 2663*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)
|- ( ( x e. A /\ ph ) -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimivw 2664*	Weaker version of rexlimiv 2662. (Contributed by FL, 19-Sep-2011.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimd 2665	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimd2 2666	Version of rexlimd 2665 with deduction version of second hypothesis. (Contributed by NM, 21-Jul-2013.) (Revised by Mario Carneiro, 8-Oct-2016.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdv 2667*	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.)
|- ( ph -> ( x e. A -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdva 2668*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdvaa 2669*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdv3a 2670*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2667. (Contributed by NM, 7-Jun-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdva2 2671*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdvw 2672*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimddv 2673*	Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ph -> E. x e. A ps )   &    |- ( ( ph /\ ( x e. A /\ ps ) ) -> ch )   =>    |- ( ph -> ch )
Theorem	rexlimivv 2674*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
|- ( ( x e. A /\ y e. B ) -> ( ph -> ps ) )   =>    |- ( E. x e. A E. y e. B ph -> ps )
Theorem	rexlimdvv 2675*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
|- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )
Theorem	rexlimdvva 2676*	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) )
Theorem	r19.26 2677	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )
Theorem	r19.27v 2678*	Restricted quantitifer version of one direction of 19.27 1614. (The other direction holds when A is inhabited, see r19.27mv 3621.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
|- ( ( A. x e. A ph /\ ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.28v 2679*	Restricted quantifier version of one direction of 19.28 1616. (The other direction holds when A is inhabited, see r19.28mv 3617.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)
|- ( ( ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.26-2 2680	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers. (Contributed by NM, 10-Aug-2004.)
|- ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A A. y e. B ph /\ A. x e. A A. y e. B ps ) )
Theorem	r19.26-3 2681	Theorem 19.26 of [Margaris] p. 90 with 3 restricted quantifiers. (Contributed by FL, 22-Nov-2010.)
|- ( A. x e. A ( ph /\ ps /\ ch ) <-> ( A. x e. A ph /\ A. x e. A ps /\ A. x e. A ch ) )
Theorem	r19.26m 2682	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers. (Contributed by NM, 22-Feb-2004.)
|- ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ps ) ) <-> ( A. x e. A ph /\ A. x e. B ps ) )
Theorem	ralbi 2683	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification. (Contributed by NM, 6-Oct-2003.)
|- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph <-> A. x e. A ps ) )
Theorem	rexbi 2684	Distribute a restricted existential quantifier over a biconditional. Theorem 19.18 of [Margaris] p. 90 with restricted quantification. (Contributed by Jim Kingdon, 21-Jan-2019.)
|- ( A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ) )
Theorem	ralbiim 2685	Split a biconditional and distribute quantifier. (Contributed by NM, 3-Jun-2012.)
|- ( A. x e. A ( ph <-> ps ) <-> ( A. x e. A ( ph -> ps ) /\ A. x e. A ( ps -> ph ) ) )
Theorem	r19.27av 2686*	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( ( A. x e. A ph /\ ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.28av 2687*	Restricted version of one direction of Theorem 19.28 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.) (Contributed by NM, 2-Apr-2004.)
|- ( ( ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
Theorem	r19.29 2688	Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)
|- ( ( A. x e. A ph /\ E. x e. A ps ) -> E. x e. A ( ph /\ ps ) )
Theorem	r19.29r 2689	Variation of Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
|- ( ( E. x e. A ph /\ A. x e. A ps ) -> E. x e. A ( ph /\ ps ) )
Theorem	ralnex2 2690	Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.)
|- ( A. x e. A A. y e. B -. ph <-> -. E. x e. A E. y e. B ph )
Theorem	r19.29af2 2691	A commonly used pattern based on r19.29 2688. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29af 2692*	A commonly used pattern based on r19.29 2688. (Contributed by Thierry Arnoux, 29-Nov-2017.)
|- F/ x ph   &    |- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29an 2693*	A commonly used pattern based on r19.29 2688. (Contributed by Thierry Arnoux, 29-Dec-2019.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ( ph /\ E. x e. A ps ) -> ch )
Theorem	r19.29a 2694*	A commonly used pattern based on r19.29 2688. (Contributed by Thierry Arnoux, 22-Nov-2017.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29d2r 2695	Theorem 19.29 of [Margaris] p. 90 with two restricted quantifiers, deduction version. (Contributed by Thierry Arnoux, 30-Jan-2017.)
|- ( ph -> A. x e. A A. y e. B ps )   &    |- ( ph -> E. x e. A E. y e. B ch )   =>    |- ( ph -> E. x e. A E. y e. B ( ps /\ ch ) )
Theorem	r19.29vva 2696*	A commonly used pattern based on r19.29 2688, version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017.)
|- ( ( ( ( ph /\ x e. A ) /\ y e. B ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A E. y e. B ps )   =>    |- ( ph -> ch )
Theorem	r19.32r 2697	One direction of Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers. For decidable propositions this is an equivalence. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- F/ x ph   =>    |- ( ( ph \/ A. x e. A ps ) -> A. x e. A ( ph \/ ps ) )
Theorem	r19.30dc 2698	Restricted quantifier version of 19.30dc 1680. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.)
|- ( ( A. x e. A ( ph \/ ps ) /\ DECID E. x e. A ps ) -> ( A. x e. A ph \/ E. x e. A ps ) )
Theorem	r19.32vr 2699*	One direction of Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers. For decidable propositions this is an equivalence, as seen at r19.32vdc 2700. (Contributed by Jim Kingdon, 19-Aug-2018.)
|- ( ( ph \/ A. x e. A ps ) -> A. x e. A ( ph \/ ps ) )
Theorem	r19.32vdc 2700*	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, where ph is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
|- (DECID ph -> ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) ) )