P. 36 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 3501-3600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rabnc 3501*	Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- ( { x e. A | ph } i^i { x e. A | -. ph } ) = (/)
Theorem	un0 3502	The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
|- ( A u. (/) ) = A
Theorem	in0 3503	The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)
|- ( A i^i (/) ) = (/)
Theorem	0in 3504	The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( (/) i^i A ) = (/)
Theorem	inv1 3505	The intersection of a class with the universal class is itself. Exercise 4.10(k) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A i^i _V ) = A
Theorem	unv 3506	The union of a class with the universal class is the universal class. Exercise 4.10(l) of [Mendelson] p. 231. (Contributed by NM, 17-May-1998.)
|- ( A u. _V ) = _V
Theorem	0ss 3507	The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
|- (/) C_ A
Theorem	ss0b 3508	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23 and its converse. (Contributed by NM, 17-Sep-2003.)
|- ( A C_ (/) <-> A = (/) )
Theorem	ss0 3509	Any subset of the empty set is empty. Theorem 5 of [Suppes] p. 23. (Contributed by NM, 13-Aug-1994.)
|- ( A C_ (/) -> A = (/) )
Theorem	sseq0 3510	A subclass of an empty class is empty. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A C_ B /\ B = (/) ) -> A = (/) )
Theorem	ssn0 3511	A class with a nonempty subclass is nonempty. (Contributed by NM, 17-Feb-2007.)
|- ( ( A C_ B /\ A =/= (/) ) -> B =/= (/) )
Theorem	abf 3512	A class builder with a false argument is empty. (Contributed by NM, 20-Jan-2012.)
|- -. ph   =>    |- { x | ph } = (/)
Theorem	eq0rdv 3513*	Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.)
|- ( ph -> -. x e. A )   =>    |- ( ph -> A = (/) )
Theorem	csbprc 3514	The proper substitution of a proper class for a set into a class results in the empty set. (Contributed by NM, 17-Aug-2018.)
|- ( -. A e. _V -> [_ A / x ]_ B = (/) )
Theorem	un00 3515	Two classes are empty iff their union is empty. (Contributed by NM, 11-Aug-2004.)
|- ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )
Theorem	vss 3516	Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( _V C_ A <-> A = _V )
Theorem	disj 3517*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )
Theorem	disjr 3518*	Two ways of saying that two classes are disjoint. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( ( A i^i B ) = (/) <-> A. x e. B -. x e. A )
Theorem	disj1 3519*	Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 19-Aug-1993.)
|- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
Theorem	reldisj 3520	Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A C_ C -> ( ( A i^i B ) = (/) <-> A C_ ( C \ B ) ) )
Theorem	disj3 3521	Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
|- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )
Theorem	disjne 3522	Members of disjoint sets are not equal. (Contributed by NM, 28-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( ( A i^i B ) = (/) /\ C e. A /\ D e. B ) -> C =/= D )
Theorem	disjel 3523	A set can't belong to both members of disjoint classes. (Contributed by NM, 28-Feb-2015.)
|- ( ( ( A i^i B ) = (/) /\ C e. A ) -> -. C e. B )
Theorem	disj2 3524	Two ways of saying that two classes are disjoint. (Contributed by NM, 17-May-1998.)
|- ( ( A i^i B ) = (/) <-> A C_ ( _V \ B ) )
Theorem	ssdisj 3525	Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007.)
|- ( ( A C_ B /\ ( B i^i C ) = (/) ) -> ( A i^i C ) = (/) )
Theorem	undisj1 3526	The union of disjoint classes is disjoint. (Contributed by NM, 26-Sep-2004.)
|- ( ( ( A i^i C ) = (/) /\ ( B i^i C ) = (/) ) <-> ( ( A u. B ) i^i C ) = (/) )
Theorem	undisj2 3527	The union of disjoint classes is disjoint. (Contributed by NM, 13-Sep-2004.)
|- ( ( ( A i^i B ) = (/) /\ ( A i^i C ) = (/) ) <-> ( A i^i ( B u. C ) ) = (/) )
Theorem	ssindif0im 3528	Subclass implies empty intersection with difference from the universal class. (Contributed by NM, 17-Sep-2003.)
|- ( A C_ B -> ( A i^i ( _V \ B ) ) = (/) )
Theorem	inelcm 3529	The intersection of classes with a common member is nonempty. (Contributed by NM, 7-Apr-1994.)
|- ( ( A e. B /\ A e. C ) -> ( B i^i C ) =/= (/) )
Theorem	minel 3530	A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994.)
|- ( ( A e. B /\ ( C i^i B ) = (/) ) -> -. A e. C )
Theorem	undif4 3531	Distribute union over difference. (Contributed by NM, 17-May-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i C ) = (/) -> ( A u. ( B \ C ) ) = ( ( A u. B ) \ C ) )
Theorem	disjssun 3532	Subset relation for disjoint classes. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) = (/) -> ( A C_ ( B u. C ) <-> A C_ C ) )
Theorem	ssdif0im 3533	Subclass implies empty difference. One direction of Exercise 7 of [TakeutiZaring] p. 22. In classical logic this would be an equivalence. (Contributed by Jim Kingdon, 2-Aug-2018.)
|- ( A C_ B -> ( A \ B ) = (/) )
Theorem	vdif0im 3534	Universal class equality in terms of empty difference. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( A = _V -> ( _V \ A ) = (/) )
Theorem	difrab0eqim 3535*	If the difference between the restricting class of a restricted class abstraction and the restricted class abstraction is empty, the restricting class is equal to this restricted class abstraction. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( V = { x e. V | ph } -> ( V \ { x e. V | ph } ) = (/) )
Theorem	inssdif0im 3536	Intersection, subclass, and difference relationship. In classical logic the converse would also hold. (Contributed by Jim Kingdon, 3-Aug-2018.)
|- ( ( A i^i B ) C_ C -> ( A i^i ( B \ C ) ) = (/) )
Theorem	difid 3537	The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.)
|- ( A \ A ) = (/)
Theorem	difidALT 3538	The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. Alternate proof of difid 3537. (Contributed by David Abernethy, 17-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A \ A ) = (/)
Theorem	dif0 3539	The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( A \ (/) ) = A
Theorem	0dif 3540	The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
|- ( (/) \ A ) = (/)
Theorem	disjdif 3541	A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)
|- ( A i^i ( B \ A ) ) = (/)
Theorem	difin0 3542	The difference of a class from its intersection is empty. Theorem 37 of [Suppes] p. 29. (Contributed by NM, 17-Aug-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( A i^i B ) \ B ) = (/)
Theorem	undif1ss 3543	Absorption of difference by union. In classical logic, as Theorem 35 of [Suppes] p. 29, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A \ B ) u. B ) C_ ( A u. B )
Theorem	undif2ss 3544	Absorption of difference by union. In classical logic, as in Part of proof of Corollary 6K of [Enderton] p. 144, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A u. ( B \ A ) ) C_ ( A u. B )
Theorem	undifabs 3545	Absorption of difference by union. (Contributed by NM, 18-Aug-2013.)
|- ( A u. ( A \ B ) ) = A
Theorem	inundifss 3546	The intersection and class difference of a class with another class are contained in the original class. In classical logic we'd be able to make a stronger statement: that everything in the original class is in the intersection or the difference (that is, this theorem would be equality rather than subset). (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A i^i B ) u. ( A \ B ) ) C_ A
Theorem	disjdif2 3547	The difference of a class and a class disjoint from it is the original class. (Contributed by BJ, 21-Apr-2019.)
|- ( ( A i^i B ) = (/) -> ( A \ B ) = A )
Theorem	difun2 3548	Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
|- ( ( A u. B ) \ B ) = ( A \ B )
Theorem	undifss 3549	Union of complementary parts into whole. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A C_ B <-> ( A u. ( B \ A ) ) C_ B )
Theorem	ssdifin0 3550	A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
|- ( A C_ ( B \ C ) -> ( A i^i C ) = (/) )
Theorem	ssdifeq0 3551	A class is a subclass of itself subtracted from another iff it is the empty set. (Contributed by Steve Rodriguez, 20-Nov-2015.)
|- ( A C_ ( B \ A ) <-> A = (/) )
Theorem	ssundifim 3552	A consequence of inclusion in the union of two classes. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( A C_ ( B u. C ) -> ( A \ B ) C_ C )
Theorem	difdifdirss 3553	Distributive law for class difference. In classical logic, as in Exercise 4.8 of [Stoll] p. 16, this would be equality rather than subset. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A \ B ) \ C ) C_ ( ( A \ C ) \ ( B \ C ) )
Theorem	uneqdifeqim 3554	Two ways that A and B can "partition" C (when A and B don't overlap and A is a part of C). In classical logic, the second implication would be a biconditional. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
Theorem	r19.2m 3555*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1662). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.)
|- ( ( E. y y e. A /\ A. x e. A ph ) -> E. x e. A ph )
Theorem	r19.2mOLD 3556*	Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1662). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) Obsolete version of r19.2m 3555 as of 7-Apr-2023. (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E. x x e. A /\ A. x e. A ph ) -> E. x e. A ph )
Theorem	r19.3rm 3557*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 19-Dec-2018.)
|- F/ x ph   =>    |- ( E. y y e. A -> ( ph <-> A. x e. A ph ) )
Theorem	r19.28m 3558*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- F/ x ph   =>    |- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( ph /\ A. x e. A ps ) ) )
Theorem	r19.3rmv 3559*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( E. y y e. A -> ( ph <-> A. x e. A ph ) )
Theorem	r19.9rmv 3560*	Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- ( E. y y e. A -> ( ph <-> E. x e. A ph ) )
Theorem	r19.28mv 3561*	Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( ph /\ A. x e. A ps ) ) )
Theorem	r19.45mv 3562*	Restricted version of Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
|- ( E. x x e. A -> ( E. x e. A ( ph \/ ps ) <-> ( ph \/ E. x e. A ps ) ) )
Theorem	r19.44mv 3563*	Restricted version of Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.)
|- ( E. y y e. A -> ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ ps ) ) )
Theorem	r19.27m 3564*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- F/ x ps   =>    |- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ ps ) ) )
Theorem	r19.27mv 3565*	Restricted quantifier version of Theorem 19.27 of [Margaris] p. 90. It is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.)
|- ( E. x x e. A -> ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ ps ) ) )
Theorem	rzal 3566*	Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( A = (/) -> A. x e. A ph )
Theorem	rexn0 3567*	Restricted existential quantification implies its restriction is nonempty (it is also inhabited as shown in rexm 3568). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- ( E. x e. A ph -> A =/= (/) )
Theorem	rexm 3568*	Restricted existential quantification implies its restriction is inhabited. (Contributed by Jim Kingdon, 16-Oct-2018.)
|- ( E. x e. A ph -> E. x x e. A )
Theorem	ralidm 3569*	Idempotent law for restricted quantifier. (Contributed by NM, 28-Mar-1997.)
|- ( A. x e. A A. x e. A ph <-> A. x e. A ph )
Theorem	ral0 3570	Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
|- A. x e. (/) ph
Theorem	ralf0 3571*	The quantification of a falsehood is vacuous when true. (Contributed by NM, 26-Nov-2005.)
|- -. ph   =>    |- ( A. x e. A ph <-> A = (/) )
Theorem	ralm 3572	Inhabited classes and restricted quantification. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- ( ( E. x x e. A -> A. x e. A ph ) <-> A. x e. A ph )
Theorem	raaanlem 3573*	Special case of raaan 3574 where A is inhabited. (Contributed by Jim Kingdon, 6-Aug-2018.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x x e. A -> ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) ) )
Theorem	raaan 3574*	Rearrange restricted quantifiers. (Contributed by NM, 26-Oct-2010.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )
Theorem	raaanv 3575*	Rearrange restricted quantifiers. (Contributed by NM, 11-Mar-1997.)
|- ( A. x e. A A. y e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. A ps ) )
Theorem	sbss 3576*	Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010.) (Proof shortened by Mario Carneiro, 14-Nov-2016.)
|- ( [ y / x ] x C_ A <-> y C_ A )
Theorem	sbcssg 3577	Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> ( [. A / x ]. B C_ C <-> [_ A / x ]_ B C_ [_ A / x ]_ C ) )
Theorem	dcun 3578	The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
|- ( ph -> DECID C e. A )   &    |- ( ph -> DECID C e. B )   =>    |- ( ph -> DECID C e. ( A u. B ) )
2.1.15  Conditional operator
Syntax	cif 3579	Extend class notation to include the conditional operator. See df-if 3580 for a description. (In older databases this was denoted "ded".)
class if ( ph , A , B )
Definition	df-if 3580*	Define the conditional operator. Read if ( ph , A , B ) as "if ph then A else B". See iftrue 3584 and iffalse 3587 for its values. In mathematical literature, this operator is rarely defined formally but is implicit in informal definitions such as "let f(x)=0 if x=0 and 1/x otherwise." In the absence of excluded middle, this will tend to be useful where ph is decidable (in the sense of df-dc 837). (Contributed by NM, 15-May-1999.)
|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
Theorem	dfif6 3581*	An alternate definition of the conditional operator df-if 3580 as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013.)
|- if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } )
Theorem	ifeq1 3582	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A = B -> if ( ph , A , C ) = if ( ph , B , C ) )
Theorem	ifeq2 3583	Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A = B -> if ( ph , C , A ) = if ( ph , C , B ) )
Theorem	iftrue 3584	Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> if ( ph , A , B ) = A )
Theorem	iftruei 3585	Inference associated with iftrue 3584. (Contributed by BJ, 7-Oct-2018.)
|- ph   =>    |- if ( ph , A , B ) = A
Theorem	iftrued 3586	Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> ch )   =>    |- ( ph -> if ( ch , A , B ) = A )
Theorem	iffalse 3587	Value of the conditional operator when its first argument is false. (Contributed by NM, 14-Aug-1999.)
|- ( -. ph -> if ( ph , A , B ) = B )
Theorem	iffalsei 3588	Inference associated with iffalse 3587. (Contributed by BJ, 7-Oct-2018.)
|- -. ph   =>    |- if ( ph , A , B ) = B
Theorem	iffalsed 3589	Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> -. ch )   =>    |- ( ph -> if ( ch , A , B ) = B )
Theorem	ifnefalse 3590	When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs versus applying iffalse 3587 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.)
|- ( A =/= B -> if ( A = B , C , D ) = D )
Theorem	elif 3591	Membership in a conditional operator. (Contributed by NM, 14-Feb-2005.)
|- ( A e. if ( ph , B , C ) <-> ( ( ph /\ A e. B ) \/ ( -. ph /\ A e. C ) ) )
Theorem	ifsbdc 3592	Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.)
|- ( if ( ph , A , B ) = A -> C = D )   &    |- ( if ( ph , A , B ) = B -> C = E )   =>    |- (DECID ph -> C = if ( ph , D , E ) )
Theorem	dfif3 3593*	Alternate definition of the conditional operator df-if 3580. Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- C = { x | ph }   =>    |- if ( ph , A , B ) = ( ( A i^i C ) u. ( B i^i ( _V \ C ) ) )
Theorem	ifssun 3594	A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , B ) C_ ( A u. B )
Theorem	ifidss 3595	A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)
|- if ( ph , A , A ) C_ A
Theorem	ifeq12 3596	Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004.)
|- ( ( A = B /\ C = D ) -> if ( ph , A , C ) = if ( ph , B , D ) )
Theorem	ifeq1d 3597	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> if ( ps , A , C ) = if ( ps , B , C ) )
Theorem	ifeq2d 3598	Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
|- ( ph -> A = B )   =>    |- ( ph -> if ( ps , C , A ) = if ( ps , C , B ) )
Theorem	ifeq12d 3599	Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> if ( ps , A , C ) = if ( ps , B , D ) )
Theorem	ifbi 3600	Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004.)
|- ( ( ph <-> ps ) -> if ( ph , A , B ) = if ( ps , A , B ) )