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	neleq12d 2501	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A e/ C <-> B e/ D ) )
Theorem	nfnel 2502	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e/ B
Theorem	nfneld 2503	Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e/ B )
Theorem	elnelne1 2504	Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020.)
|- ( ( A e. B /\ A e/ C ) -> B =/= C )
Theorem	elnelne2 2505	Two classes are different if they don't belong to the same class. (Contributed by AV, 28-Jan-2020.)
|- ( ( A e. C /\ B e/ C ) -> A =/= B )
Theorem	nelcon3d 2506	Contrapositive law deduction for negated membership. (Contributed by AV, 28-Jan-2020.)
|- ( ph -> ( A e. B -> C e. D ) )   =>    |- ( ph -> ( C e/ D -> A e/ B ) )
Theorem	elnelall 2507	A contradiction concerning membership implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A e. B -> ( A e/ B -> ph ) )
2.1.5  Restricted quantification
Syntax	wral 2508	Extend wff notation to include restricted universal quantification.
wff A. x e. A ph
Syntax	wrex 2509	Extend wff notation to include restricted existential quantification.
wff E. x e. A ph
Syntax	wreu 2510	Extend wff notation to include restricted existential uniqueness.
wff E! x e. A ph
Syntax	wrmo 2511	Extend wff notation to include restricted "at most one".
wff E* x e. A ph
Syntax	crab 2512	Extend class notation to include the restricted class abstraction (class builder).
class { x e. A | ph }
Definition	df-ral 2513	Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
Definition	df-rex 2514	Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
Definition	df-reu 2515	Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
Definition	df-rmo 2516	Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
Definition	df-rab 2517	Define a restricted class abstraction (class builder), which is the class of all x in A such that ph is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
Theorem	ralnex 2518	Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
|- ( A. x e. A -. ph <-> -. E. x e. A ph )
Theorem	rexnalim 2519	Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x e. A -. ph -> -. A. x e. A ph )
Theorem	nnral 2520	The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1695. (Contributed by Jim Kingdon, 1-Aug-2024.)
|- ( -. -. A. x e. A ph -> A. x e. A -. -. ph )
Theorem	dfrex2dc 2521	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 29-Jun-2022.)
|- (DECID E. x e. A ph -> ( E. x e. A ph <-> -. A. x e. A -. ph ) )
Theorem	ralexim 2522	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( A. x e. A ph -> -. E. x e. A -. ph )
Theorem	rexalim 2523	Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
|- ( E. x e. A ph -> -. A. x e. A -. ph )
Theorem	ralbida 2524	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbida 2525	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 6-Oct-2003.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidva 2526*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidva 2527*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbid 2528	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbid 2529	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 27-Jun-1998.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidv 2530*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )
Theorem	rexbidv 2531*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 20-Nov-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )
Theorem	ralbidv2 2532*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.)
|- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexbidv2 2533*	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.)
|- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	ralbid2 2534	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )   =>    |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )
Theorem	rexbid2 2535	Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
|- F/ x ph   &    |- ( ph -> ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) ) )   =>    |- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )
Theorem	ralbii 2536	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( A. x e. A ph <-> A. x e. A ps )
Theorem	rexbii 2537	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( E. x e. A ph <-> E. x e. A ps )
Theorem	2ralbii 2538	Inference adding two restricted universal quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
|- ( ph <-> ps )   =>    |- ( A. x e. A A. y e. B ph <-> A. x e. A A. y e. B ps )
Theorem	2rexbii 2539	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
|- ( ph <-> ps )   =>    |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )
Theorem	ralbii2 2540	Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)
|- ( ( x e. A -> ph ) <-> ( x e. B -> ps ) )   =>    |- ( A. x e. A ph <-> A. x e. B ps )
Theorem	rexbii2 2541	Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)
|- ( ( x e. A /\ ph ) <-> ( x e. B /\ ps ) )   =>    |- ( E. x e. A ph <-> E. x e. B ps )
Theorem	raleqbii 2542	Equality deduction for restricted universal quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
|- A = B   &    |- ( ps <-> ch )   =>    |- ( A. x e. A ps <-> A. x e. B ch )
Theorem	rexeqbii 2543	Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017.)
|- A = B   &    |- ( ps <-> ch )   =>    |- ( E. x e. A ps <-> E. x e. B ch )
Theorem	ralbiia 2544	Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. x e. A ps )
Theorem	rexbiia 2545	Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
|- ( x e. A -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. x e. A ps )
Theorem	2rexbiia 2546*	Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 1-Aug-2004.)
|- ( ( x e. A /\ y e. B ) -> ( ph <-> ps ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. x e. A E. y e. B ps )
Theorem	r2alf 2547*	Double restricted universal quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ y A   =>    |- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )
Theorem	r2exf 2548*	Double restricted existential quantification. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ y A   =>    |- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
Theorem	r2al 2549*	Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.)
|- ( A. x e. A A. y e. B ph <-> A. x A. y ( ( x e. A /\ y e. B ) -> ph ) )
Theorem	r2ex 2550*	Double restricted existential quantification. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A E. y e. B ph <-> E. x E. y ( ( x e. A /\ y e. B ) /\ ph ) )
Theorem	2ralbida 2551*	Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 24-Feb-2004.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ( 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	2ralbidva 2552*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)
|- ( ( 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	2rexbidva 2553*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.)
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )
Theorem	2ralbidv 2554*	Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )
Theorem	2rexbidv 2555*	Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )
Theorem	rexralbidv 2556*	Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x e. A A. y e. B ps <-> E. x e. A A. y e. B ch ) )
Theorem	ralinexa 2557	A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.)
|- ( A. x e. A ( ph -> -. ps ) <-> -. E. x e. A ( ph /\ ps ) )
Theorem	risset 2558*	Two ways to say " A belongs to B". (Contributed by NM, 22-Nov-1994.)
|- ( A e. B <-> E. x e. B x = A )
Theorem	hbral 2559	Bound-variable hypothesis builder for restricted quantification. (Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy, 13-Dec-2009.)
|- ( y e. A -> A. x y e. A )   &    |- ( ph -> A. x ph )   =>    |- ( A. y e. A ph -> A. x A. y e. A ph )
Theorem	hbra1 2560	x is not free in A. x e. A ph. (Contributed by NM, 18-Oct-1996.)
|- ( A. x e. A ph -> A. x A. x e. A ph )
Theorem	nfra1 2561	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 2562*	Not-free for restricted universal quantification where x and y are distinct. See nfraldya 2565 for a version with y and A distinct instead. (Contributed by NM, 15-Feb-2013.) (Revised by GG, 10-Jan-2024.)
|- F/ y ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x A. y e. A ps )
Theorem	nfraldxy 2563*	Old name for nfraldw 2562. (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 2564*	Not-free for restricted existential quantification where x and y are distinct. See nfrexdya 2566 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 2565*	Not-free for restricted universal quantification where y and A are distinct. See nfraldxy 2563 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 2566*	Not-free for restricted existential quantification where y and A are distinct. See nfrexdxy 2564 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 2567*	Bound-variable hypothesis builder for restricted quantification. See nfralya 2570 for a version with y and A distinct instead of x and y. (Contributed by NM, 1-Sep-1999.) (Revised by GG, 10-Jan-2024.)
|- F/_ x A   &    |- F/ x ph   =>    |- F/ x A. y e. A ph
Theorem	nfralxy 2568*	Old name for nfralw 2567. (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	nfrexw 2569*	Not-free for restricted existential quantification where x and y are distinct. See nfrexya 2571 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 2570*	Not-free for restricted universal quantification where y and A are distinct. See nfralxy 2568 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 2571*	Not-free for restricted existential quantification where y and A are distinct. See nfrexw 2569 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 2572*	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 2573	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 2574*	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 2575	Universal quantification implies restricted quantification. (Contributed by NM, 20-Oct-2006.)
|- ( A. x ph -> A. x e. A ph )
Theorem	rexex 2576	Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
|- ( E. x e. A ph -> E. x ph )
Theorem	rsp 2577	Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|- ( A. x e. A ph -> ( x e. A -> ph ) )
Theorem	rspa 2578	Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A. x e. A ph /\ x e. A ) -> ph )
Theorem	rspe 2579	Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|- ( ( x e. A /\ ph ) -> E. x e. A ph )
Theorem	rsp2 2580	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 2581	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 2582	Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- A. x e. A ph   =>    |- ( x e. A -> ph )
Theorem	rgen 2583	Generalization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)
|- ( x e. A -> ph )   =>    |- A. x e. A ph
Theorem	rgen2a 2584*	Generalization rule for restricted quantification. Note that x and y are not required to be disjoint. This proof illustrates the use of dvelim 2068. Usage of rgen2 2616 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 2585	Generalization rule for restricted quantification. (Contributed by NM, 18-Jun-2014.)
|- ph   =>    |- A. x e. A ph
Theorem	rgen2w 2586	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 2587	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 2588	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 2589	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 2590	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 2591	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 2592	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 2593	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 2594	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 2595	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 2596	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 2597*	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 2598*	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 2599*	Deduction doubly quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1503). (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 2600*	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 ) )