P. 26 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2501-2600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	r3al 2501*	Triple restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
|- ( A. x e. A A. y e. B A. z e. C ph <-> A. x A. y A. z ( ( x e. A /\ y e. B /\ z e. C ) -> ph ) )
Theorem	alral 2502	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
|- ( A. x ph -> A. x e. A ph )
Theorem	rexex 2503	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A ph -> E. x ph )
Theorem	rsp 2504	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|- ( A. x e. A ph -> ( x e. A -> ph ) )
Theorem	rspa 2505	Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A. x e. A ph /\ x e. A ) -> ph )
Theorem	rspe 2506	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ( ( x e. A /\ ph ) -> E. x e. A ph )
Theorem	rsp2 2507	Restricted specialization. (Contributed by NM, 11-Feb-1997.)
|- ( A. x e. A A. y e. B ph -> ( ( x e. A /\ y e. B ) -> ph ) )
Theorem	rsp2e 2508	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 2509	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A. x e. A ph   =>    |- ( x e. A -> ph )
Theorem	rgen 2510	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- ( x e. A -> ph )   =>    |- A. x e. A ph
Theorem	rgen2a 2511*	Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 1997. Usage of rgen2 2543 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 2512	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A ph
Theorem	rgen2w 2513	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 2514	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 2515	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 2516	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 2517	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 2518	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 2519	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 2520	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 2521	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 2522	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 2523	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 2524*	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 2525*	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 2526*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1437). (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 2527*	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 2528	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 2529*	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 2530*	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 2531*	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 2532	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 2533	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 2534*	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 2535	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 2536*	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 2537*	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 2538*	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 2539*	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 2540*	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 2541*	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 2542*	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 2543*	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 2544*	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 2545	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 2546	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 2547	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 2548	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 2549	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 2550*	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 2551	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 2552	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 2553	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 2554	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 2555	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 2556*	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 2557*	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 2558*	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 2559*	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 2560*	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 2561*	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 2562*	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	r19.12 2563*	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 2564	Closed theorem form of r19.23 2565. (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 2565	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 2566*	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 2567	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 2568*	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 2569*	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 2570*	Weaker version of rexlimiv 2568. (Contributed by FL, 19-Sep-2011.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimd 2571	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 2572	Version of rexlimd 2571 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 2573*	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 2574*	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 2575*	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 2576*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2573. (Contributed by NM, 7-Jun-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdva2 2577*	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 2578*	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 2579*	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 2580*	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 2581*	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 2582*	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 2583	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 2584*	Restricted quantitifer version of one direction of 19.27 1541. (The other direction holds when A is inhabited, see r19.27mv 3490.) (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 2585*	Restricted quantifier version of one direction of 19.28 1543. (The other direction holds when A is inhabited, see r19.28mv 3486.) (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 2586	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 2587	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 2588	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 2589	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 2590	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 2591	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 2592*	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 2593*	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 2594	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 2595	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 2596	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 2597	A commonly used pattern based on r19.29 2594 (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 2598*	A commonly used pattern based on r19.29 2594 (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 2599*	A commonly used pattern based on r19.29 2594. (Contributed by Thierry Arnoux, 29-Dec-2019.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   =>    |- ( ( ph /\ E. x e. A ps ) -> ch )
Theorem	r19.29a 2600*	A commonly used pattern based on r19.29 2594 (Contributed by Thierry Arnoux, 22-Nov-2017.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )