P. 25 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfrexdya 2401*	Not-free for restricted existential quantification where y and A are distinct. See nfrexdxy 2399 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	nfralxy 2402*	Not-free for restricted universal quantification where x and y are distinct. See nfralya 2404 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x A. y e. A ph
Theorem	nfrexxy 2403*	Not-free for restricted existential quantification where x and y are distinct. See nfrexya 2405 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 2404*	Not-free for restricted universal quantification where y and A are distinct. See nfralxy 2402 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 2405*	Not-free for restricted existential quantification where y and A are distinct. See nfrexxy 2403 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 2406*	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 2407	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 2408*	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 2409	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
|- ( A. x ph -> A. x e. A ph )
Theorem	rexex 2410	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A ph -> E. x ph )
Theorem	rsp 2411	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|- ( A. x e. A ph -> ( x e. A -> ph ) )
Theorem	rspe 2412	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ( ( x e. A /\ ph ) -> E. x e. A ph )
Theorem	rsp2 2413	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 2414	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 2415	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A. x e. A ph   =>    |- ( x e. A -> ph )
Theorem	rgen 2416	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- ( x e. A -> ph )   =>    |- A. x e. A ph
Theorem	rgen2a 2417*	Generalization rule for restricted quantification. Note that x and y needn't be distinct (and illustrates the use of dvelimor 1935). (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.)
|- ( ( x e. A /\ y e. A ) -> ph )   =>    |- A. x e. A A. y e. A ph
Theorem	rgenw 2418	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A ph
Theorem	rgen2w 2419	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 2420	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 2421	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 2422	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 2423	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 2424	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 2425	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 2426	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	ral2imi 2427	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 2428	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 2429*	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 2430*	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	ralimdv2 2431*	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 2432	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 2433*	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 2434*	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 2435*	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 2436	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 2437	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 2438*	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 2439	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 2440*	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 2441*	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 2442*	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 2443*	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 2444*	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 2445*	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 2446*	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 2447*	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 2448*	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 2449	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 2450	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 2451	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 2452	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 2453	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 2454*	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 2455	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 2456	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 2457	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 2458	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 2459	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 2460*	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 2461*	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 2462*	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 2463*	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 2464*	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	reximddv2 2465*	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 2466*	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 2467	Closed theorem form of r19.23 2468. (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 2468	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 2469*	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 2470	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 2471*	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 2472*	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 2473*	Weaker version of rexlimiv 2471. (Contributed by FL, 19-Sep-2011.)
|- ( ph -> ps )   =>    |- ( E. x e. A ph -> ps )
Theorem	rexlimd 2474	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 2475	Version of rexlimd 2474 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 2476*	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 2477*	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 2478*	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 2479*	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2476. (Contributed by NM, 7-Jun-2015.)
|- ( ( ph /\ x e. A /\ ps ) -> ch )   =>    |- ( ph -> ( E. x e. A ps -> ch ) )
Theorem	rexlimdvw 2480*	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 2481*	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 2482*	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 2483*	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 2484*	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 2485	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.26-2 2486	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 2487	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 2488	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 2489	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 2490	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 2491	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 2492*	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 2493*	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 2494	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 2495	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	r19.29af2 2496	A commonly used pattern based on r19.29 2494 (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 2497*	A commonly used pattern based on r19.29 2494 (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.29a 2498*	A commonly used pattern based on r19.29 2494 (Contributed by Thierry Arnoux, 22-Nov-2017.)
|- ( ( ( ph /\ x e. A ) /\ ps ) -> ch )   &    |- ( ph -> E. x e. A ps )   =>    |- ( ph -> ch )
Theorem	r19.29d2r 2499	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 2500*	A commonly used pattern based on r19.29 2494, 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 )