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	nfra1 2501	x is not free in A. x e. A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x A. x e. A ph
Theorem	nfraldw 2502*	Not-free for restricted universal quantification where x and y are distinct. See nfraldya 2505 for a version with y and A distinct instead. (Contributed by NM, 15-Feb-2013.) (Revised by Gino Giotto, 10-Jan-2024.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y e. A ps )
Theorem	nfraldxy 2503*	Old name for nfraldw 2502. (Contributed by Jim Kingdon, 29-May-2018.) (New usage is discouraged.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y e. A ps )
Theorem	nfrexdxy 2504*	Not-free for restricted existential quantification where x and y are distinct. See nfrexdya 2506 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y e. A ps )
Theorem	nfraldya 2505*	Not-free for restricted universal quantification where y and A are distinct. See nfraldxy 2503 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y e. A ps )
Theorem	nfrexdya 2506*	Not-free for restricted existential quantification where y and A are distinct. See nfrexdxy 2504 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E. y e. A ps )
Theorem	nfralw 2507*	Bound-variable hypothesis builder for restricted quantification. See nfralya 2510 for a version with y and A distinct instead of x and y. (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-2024.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x A. y e. A ph
Theorem	nfralxy 2508*	Old name for nfralw 2507. (Contributed by Jim Kingdon, 30-May-2018.) (New usage is discouraged.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x A. y e. A ph
Theorem	nfrexxy 2509*	Not-free for restricted existential quantification where x and y are distinct. See nfrexya 2511 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x E. y e. A ph
Theorem	nfralya 2510*	Not-free for restricted universal quantification where y and A are distinct. See nfralxy 2508 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x A. y e. A ph
Theorem	nfrexya 2511*	Not-free for restricted existential quantification where y and A are distinct. See nfrexxy 2509 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x E. y e. A ph
Theorem	nfra2xy 2512*	Not-free given two restricted quantifiers. (Contributed by Jim Kingdon, 20-Aug-2018.)
|- F/ y A. x e. A A. y e. B ph
Theorem	nfre1 2513	x is not free in E. x e. A ph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E. x e. A ph
Theorem	r3al 2514*	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 2515	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
|- ( A. x ph -> A. x e. A ph )
Theorem	rexex 2516	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A ph -> E. x ph )
Theorem	rsp 2517	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|- ( A. x e. A ph -> ( x e. A -> ph ) )
Theorem	rspa 2518	Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A. x e. A ph /\ x e. A ) -> ph )
Theorem	rspe 2519	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ( ( x e. A /\ ph ) -> E. x e. A ph )
Theorem	rsp2 2520	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 2521	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 2522	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A. x e. A ph   =>    |- ( x e. A -> ph )
Theorem	rgen 2523	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- ( x e. A -> ph )   =>    |- A. x e. A ph
Theorem	rgen2a 2524*	Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2010. Usage of rgen2 2556 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 2525	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A ph
Theorem	rgen2w 2526	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 2527	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 2528	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 2529	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 2530	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 2531	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 2532	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 2533	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 2534	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 2535	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 2536	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 2537*	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 2538*	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 2539*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1450). (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 2540*	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 2541	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 2542*	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 2543*	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 2544*	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 2545	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 2546	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 2547*	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 2548	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 2549*	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 2550*	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 2551*	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 2552*	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 2553*	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 2554*	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 2555*	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 2556*	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 2557*	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 2558	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 2559	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 2560	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 2561	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 2562	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 2563*	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 2564	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 2565	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 2566	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 2567	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 2568	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 2569*	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 2570*	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 2571*	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 2572*	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 2573*	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 2574*	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 2575*	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 2576*	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 2577	Closed theorem form of r19.23 2578. (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 2578	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 2579*	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 2580	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 2581*	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 2582*	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 2583*	Weaker version of rexlimiv 2581. (Contributed by FL, 19-Sep-2011.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimd 2584	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 2585	Version of rexlimd 2584 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 2586*	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 2587*	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 2588*	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 2589*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2586. (Contributed by NM, 7-Jun-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdva2 2590*	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 2591*	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 2592*	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 2593*	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 2594*	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 2595*	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 2596	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 2597*	Restricted quantitifer version of one direction of 19.27 1554. (The other direction holds when A is inhabited, see r19.27mv 3511.) (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 2598*	Restricted quantifier version of one direction of 19.28 1556. (The other direction holds when A is inhabited, see r19.28mv 3507.) (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 2599	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 2600	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 ) )