P. 33 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3201-3300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elinel1 3201	Membership in an intersection implies membership in the first set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( B i^i C ) -> A e. B )
Theorem	elinel2 3202	Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( B i^i C ) -> A e. C )
Theorem	elin2 3203	Membership in a class defined as an intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = ( B i^i C )   =>    |- ( A e. X <-> ( A e. B /\ A e. C ) )
Theorem	elin1d 3204	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
|- ( ph -> X e. ( A i^i B ) )   =>    |- ( ph -> X e. A )
Theorem	elin2d 3205	Elementhood in the first set of an intersection - deduction version. (Contributed by Thierry Arnoux, 3-May-2020.)
|- ( ph -> X e. ( A i^i B ) )   =>    |- ( ph -> X e. B )
Theorem	elin3 3206	Membership in a class defined as a ternary intersection. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- X = ( ( B i^i C ) i^i D )   =>    |- ( A e. X <-> ( A e. B /\ A e. C /\ A e. D ) )
Theorem	incom 3207	Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i B ) = ( B i^i A )
Theorem	ineqri 3208*	Inference from membership to intersection. (Contributed by NM, 5-Aug-1993.)
|- ( ( x e. A /\ x e. B ) <-> x e. C )   =>    |- ( A i^i B ) = C
Theorem	ineq1 3209	Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993.)
|- ( A = B -> ( A i^i C ) = ( B i^i C ) )
Theorem	ineq2 3210	Equality theorem for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- ( A = B -> ( C i^i A ) = ( C i^i B ) )
Theorem	ineq12 3211	Equality theorem for intersection of two classes. (Contributed by NM, 8-May-1994.)
|- ( ( A = B /\ C = D ) -> ( A i^i C ) = ( B i^i D ) )
Theorem	ineq1i 3212	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>    |- ( A i^i C ) = ( B i^i C )
Theorem	ineq2i 3213	Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
|- A = B   =>    |- ( C i^i A ) = ( C i^i B )
Theorem	ineq12i 3214	Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
|- A = B   &    |- C = D   =>    |- ( A i^i C ) = ( B i^i D )
Theorem	ineq1d 3215	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A i^i C ) = ( B i^i C ) )
Theorem	ineq2d 3216	Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C i^i A ) = ( C i^i B ) )
Theorem	ineq12d 3217	Equality deduction for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A i^i C ) = ( B i^i D ) )
Theorem	ineqan12d 3218	Equality deduction for intersection of two classes. (Contributed by NM, 7-Feb-2007.)
|- ( ph -> A = B )   &    |- ( ps -> C = D )   =>    |- ( ( ph /\ ps ) -> ( A i^i C ) = ( B i^i D ) )
Theorem	dfss1 3219	A frequently-used variant of subclass definition df-ss 3026. (Contributed by NM, 10-Jan-2015.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	dfss5 3220	Another definition of subclasshood. Similar to df-ss 3026, dfss 3027, and dfss1 3219. (Contributed by David Moews, 1-May-2017.)
|- ( A C_ B <-> A = ( B i^i A ) )
Theorem	nfin 3221	Bound-variable hypothesis builder for the intersection of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/_ x ( A i^i B )
Theorem	csbing 3222	Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.)
|- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )
Theorem	rabbi2dva 3223*	Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
|- ( ( ph /\ x e. A ) -> ( x e. B <-> ps ) )   =>    |- ( ph -> ( A i^i B ) = { x e. A | ps } )
Theorem	inidm 3224	Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i A ) = A
Theorem	inass 3225	Associative law for intersection of classes. Exercise 9 of [TakeutiZaring] p. 17. (Contributed by NM, 3-May-1994.)
|- ( ( A i^i B ) i^i C ) = ( A i^i ( B i^i C ) )
Theorem	in12 3226	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.)
|- ( A i^i ( B i^i C ) ) = ( B i^i ( A i^i C ) )
Theorem	in32 3227	A rearrangement of intersection. (Contributed by NM, 21-Apr-2001.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i B )
Theorem	in13 3228	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- ( A i^i ( B i^i C ) ) = ( C i^i ( B i^i A ) )
Theorem	in31 3229	A rearrangement of intersection. (Contributed by NM, 27-Aug-2012.)
|- ( ( A i^i B ) i^i C ) = ( ( C i^i B ) i^i A )
Theorem	inrot 3230	Rotate the intersection of 3 classes. (Contributed by NM, 27-Aug-2012.)
|- ( ( A i^i B ) i^i C ) = ( ( C i^i A ) i^i B )
Theorem	in4 3231	Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001.)
|- ( ( A i^i B ) i^i ( C i^i D ) ) = ( ( A i^i C ) i^i ( B i^i D ) )
Theorem	inindi 3232	Intersection distributes over itself. (Contributed by NM, 6-May-1994.)
|- ( A i^i ( B i^i C ) ) = ( ( A i^i B ) i^i ( A i^i C ) )
Theorem	inindir 3233	Intersection distributes over itself. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) i^i C ) = ( ( A i^i C ) i^i ( B i^i C ) )
Theorem	sseqin2 3234	A relationship between subclass and intersection. Similar to Exercise 9 of [TakeutiZaring] p. 18. (Contributed by NM, 17-May-1994.)
|- ( A C_ B <-> ( B i^i A ) = A )
Theorem	inss1 3235	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- ( A i^i B ) C_ A
Theorem	inss2 3236	The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.)
|- ( A i^i B ) C_ B
Theorem	ssin 3237	Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
Theorem	ssini 3238	An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)
|- A C_ B   &    |- A C_ C   =>    |- A C_ ( B i^i C )
Theorem	ssind 3239	A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A C_ B )   &    |- ( ph -> A C_ C )   =>    |- ( ph -> A C_ ( B i^i C ) )
Theorem	ssrin 3240	Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
Theorem	sslin 3241	Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)
|- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )
Theorem	ssrind 3242	Add right intersection to subclass relation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ B )   =>    |- ( ph -> ( A i^i C ) C_ ( B i^i C ) )
Theorem	ss2in 3243	Intersection of subclasses. (Contributed by NM, 5-May-2000.)
|- ( ( A C_ B /\ C C_ D ) -> ( A i^i C ) C_ ( B i^i D ) )
Theorem	ssinss1 3244	Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)
|- ( A C_ C -> ( A i^i B ) C_ C )
Theorem	inss 3245	Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014.)
|- ( ( A C_ C \/ B C_ C ) -> ( A i^i B ) C_ C )
2.1.13.4  Combinations of difference, union, and intersection of two classes
Theorem	unabs 3246	Absorption law for union. (Contributed by NM, 16-Apr-2006.)
|- ( A u. ( A i^i B ) ) = A
Theorem	inabs 3247	Absorption law for intersection. (Contributed by NM, 16-Apr-2006.)
|- ( A i^i ( A u. B ) ) = A
Theorem	dfss4st 3248*	Subclass defined in terms of class difference. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A. xSTAB x e. A -> ( A C_ B <-> ( B \ ( B \ A ) ) = A ) )
Theorem	ssddif 3249	Double complement and subset. Similar to ddifss 3253 but inside a class B instead of the universal class _V. In classical logic the subset operation on the right hand side could be an equality (that is, A C_ B <-> ( B \ ( B \ A ) ) = A). (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A C_ B <-> A C_ ( B \ ( B \ A ) ) )
Theorem	unssdif 3250	Union of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) \ B ) )
Theorem	inssdif 3251	Intersection of two classes and class difference. In classical logic this would be an equality. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- ( A i^i B ) C_ ( A \ ( _V \ B ) )
Theorem	difin 3252	Difference with intersection. Theorem 33 of [Suppes] p. 29. (Contributed by NM, 31-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A \ ( A i^i B ) ) = ( A \ B )
Theorem	ddifss 3253	Double complement under universal class. In classical logic (or given an additional hypothesis, as in ddifnel 3146), this is equality rather than subset. (Contributed by Jim Kingdon, 24-Jul-2018.)
|- A C_ ( _V \ ( _V \ A ) )
Theorem	unssin 3254	Union as a subset of class complement and intersection (De Morgan's law). One direction of the definition of union in [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
|- ( A u. B ) C_ ( _V \ ( ( _V \ A ) i^i ( _V \ B ) ) )
Theorem	inssun 3255	Intersection in terms of class difference and union (De Morgan's law). Similar to Exercise 4.10(n) of [Mendelson] p. 231. This would be an equality, rather than subset, in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
|- ( A i^i B ) C_ ( _V \ ( ( _V \ A ) u. ( _V \ B ) ) )
Theorem	inssddif 3256	Intersection of two classes and class difference. In classical logic, such as Exercise 4.10(q) of [Mendelson] p. 231, this is an equality rather than subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
|- ( A i^i B ) C_ ( A \ ( A \ B ) )
Theorem	invdif 3257	Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( _V \ B ) ) = ( A \ B )
Theorem	indif 3258	Intersection with class difference. Theorem 34 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A i^i ( A \ B ) ) = ( A \ B )
Theorem	indif2 3259	Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
|- ( A i^i ( B \ C ) ) = ( ( A i^i B ) \ C )
Theorem	indif1 3260	Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015.)
|- ( ( A \ C ) i^i B ) = ( ( A i^i B ) \ C )
Theorem	indifcom 3261	Commutation law for intersection and difference. (Contributed by Scott Fenton, 18-Feb-2013.)
|- ( A i^i ( B \ C ) ) = ( B i^i ( A \ C ) )
Theorem	indi 3262	Distributive law for intersection over union. Exercise 10 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A i^i ( B u. C ) ) = ( ( A i^i B ) u. ( A i^i C ) )
Theorem	undi 3263	Distributive law for union over intersection. Exercise 11 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A u. ( B i^i C ) ) = ( ( A u. B ) i^i ( A u. C ) )
Theorem	indir 3264	Distributive law for intersection over union. Theorem 28 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ( ( A u. B ) i^i C ) = ( ( A i^i C ) u. ( B i^i C ) )
Theorem	undir 3265	Distributive law for union over intersection. Theorem 29 of [Suppes] p. 27. (Contributed by NM, 30-Sep-2002.)
|- ( ( A i^i B ) u. C ) = ( ( A u. C ) i^i ( B u. C ) )
Theorem	uneqin 3266	Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A u. B ) = ( A i^i B ) <-> A = B )
Theorem	difundi 3267	Distributive law for class difference. Theorem 39 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) i^i ( A \ C ) )
Theorem	difundir 3268	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A u. B ) \ C ) = ( ( A \ C ) u. ( B \ C ) )
Theorem	difindiss 3269	Distributive law for class difference. In classical logic, for example, theorem 40 of [Suppes] p. 29, this is an equality instead of subset. (Contributed by Jim Kingdon, 26-Jul-2018.)
|- ( ( A \ B ) u. ( A \ C ) ) C_ ( A \ ( B i^i C ) )
Theorem	difindir 3270	Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
|- ( ( A i^i B ) \ C ) = ( ( A \ C ) i^i ( B \ C ) )
Theorem	indifdir 3271	Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
|- ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )
Theorem	difdif2ss 3272	Set difference with a set difference. In classical logic this would be equality rather than subset. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( A \ B ) u. ( A i^i C ) ) C_ ( A \ ( B \ C ) )
Theorem	undm 3273	De Morgan's law for union. Theorem 5.2(13) of [Stoll] p. 19. (Contributed by NM, 18-Aug-2004.)
|- ( _V \ ( A u. B ) ) = ( ( _V \ A ) i^i ( _V \ B ) )
Theorem	indmss 3274	De Morgan's law for intersection. In classical logic, this would be equality rather than subset, as in Theorem 5.2(13') of [Stoll] p. 19. (Contributed by Jim Kingdon, 27-Jul-2018.)
|- ( ( _V \ A ) u. ( _V \ B ) ) C_ ( _V \ ( A i^i B ) )
Theorem	difun1 3275	A relationship involving double difference and union. (Contributed by NM, 29-Aug-2004.)
|- ( A \ ( B u. C ) ) = ( ( A \ B ) \ C )
Theorem	undif3ss 3276	A subset relationship involving class union and class difference. In classical logic, this would be equality rather than subset, as in the first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- ( A u. ( B \ C ) ) C_ ( ( A u. B ) \ ( C \ A ) )
Theorem	difin2 3277	Represent a set difference as an intersection with a larger difference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A C_ C -> ( A \ B ) = ( ( C \ B ) i^i A ) )
Theorem	dif32 3278	Swap second and third argument of double difference. (Contributed by NM, 18-Aug-2004.)
|- ( ( A \ B ) \ C ) = ( ( A \ C ) \ B )
Theorem	difabs 3279	Absorption-like law for class difference: you can remove a class only once. (Contributed by FL, 2-Aug-2009.)
|- ( ( A \ B ) \ B ) = ( A \ B )
Theorem	symdif1 3280	Two ways to express symmetric difference. This theorem shows the equivalence of the definition of symmetric difference in [Stoll] p. 13 and the restated definition in Example 4.1 of [Stoll] p. 262. (Contributed by NM, 17-Aug-2004.)
|- ( ( A \ B ) u. ( B \ A ) ) = ( ( A u. B ) \ ( A i^i B ) )
2.1.13.5  Class abstractions with difference, union, and intersection of two classes
Theorem	symdifxor 3281*	Expressing symmetric difference with exclusive-or or two differences. (Contributed by Jim Kingdon, 28-Jul-2018.)
|- ( ( A \ B ) u. ( B \ A ) ) = { x | ( x e. A \/_ x e. B ) }
Theorem	unab 3282	Union of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } u. { x | ps } ) = { x | ( ph \/ ps ) }
Theorem	inab 3283	Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } i^i { x | ps } ) = { x | ( ph /\ ps ) }
Theorem	difab 3284	Difference of two class abstractions. (Contributed by NM, 23-Oct-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( { x | ph } \ { x | ps } ) = { x | ( ph /\ -. ps ) }
Theorem	notab 3285	A class builder defined by a negation. (Contributed by FL, 18-Sep-2010.)
|- { x | -. ph } = ( _V \ { x | ph } )
Theorem	unrab 3286	Union of two restricted class abstractions. (Contributed by NM, 25-Mar-2004.)
|- ( { x e. A | ph } u. { x e. A | ps } ) = { x e. A | ( ph \/ ps ) }
Theorem	inrab 3287	Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.)
|- ( { x e. A | ph } i^i { x e. A | ps } ) = { x e. A | ( ph /\ ps ) }
Theorem	inrab2 3288*	Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007.)
|- ( { x e. A | ph } i^i B ) = { x e. ( A i^i B ) | ph }
Theorem	difrab 3289	Difference of two restricted class abstractions. (Contributed by NM, 23-Oct-2004.)
|- ( { x e. A | ph } \ { x e. A | ps } ) = { x e. A | ( ph /\ -. ps ) }
Theorem	dfrab2 3290*	Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003.)
|- { x e. A | ph } = ( { x | ph } i^i A )
Theorem	dfrab3 3291*	Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- { x e. A | ph } = ( A i^i { x | ph } )
Theorem	notrab 3292*	Complementation of restricted class abstractions. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A \ { x e. A | ph } ) = { x e. A | -. ph }
Theorem	dfrab3ss 3293*	Restricted class abstraction with a common superset. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 8-Nov-2015.)
|- ( A C_ B -> { x e. A | ph } = ( A i^i { x e. B | ph } ) )
Theorem	rabun2 3294	Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015.)
|- { x e. ( A u. B ) | ph } = ( { x e. A | ph } u. { x e. B | ph } )
2.1.13.6  Restricted uniqueness with difference, union, and intersection
Theorem	reuss2 3295*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 20-Oct-2005.)
|- ( ( ( A C_ B /\ A. x e. A ( ph -> ps ) ) /\ ( E. x e. A ph /\ E! x e. B ps ) ) -> E! x e. A ph )
Theorem	reuss 3296*	Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999.)
|- ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> E! x e. A ph )
Theorem	reuun1 3297*	Transfer uniqueness to a smaller class. (Contributed by NM, 21-Oct-2005.)
|- ( ( E. x e. A ph /\ E! x e. ( A u. B ) ( ph \/ ps ) ) -> E! x e. A ph )
Theorem	reuun2 3298*	Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005.)
|- ( -. E. x e. B ph -> ( E! x e. ( A u. B ) ph <-> E! x e. A ph ) )
Theorem	reupick 3299*	Restricted uniqueness "picks" a member of a subclass. (Contributed by NM, 21-Aug-1999.)
|- ( ( ( A C_ B /\ ( E. x e. A ph /\ E! x e. B ph ) ) /\ ph ) -> ( x e. A <-> x e. B ) )
Theorem	reupick3 3300*	Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 19-Nov-2016.)
|- ( ( E! x e. A ph /\ E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ph -> ps ) )