P. 323 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32201-32300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-prrngo 32201	Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- PrRing = { r e. RingOps | { (GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }
Definition	df-dmn 32202	Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- Dmn = ( PrRing i^i Com2 )
Theorem	isprrngo 32203	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- Z = (GId ` G )   =>    |- ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )
Theorem	prrngorngo 32204	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. PrRing -> R e. RingOps )
Theorem	smprngopr 32205	A simple ring (one whose only ideals are 0 and R) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( ( R e. RingOps /\ U =/= Z /\ ( Idl ` R ) = { { Z } , X } ) -> R e. PrRing )
Theorem	divrngpr 32206	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. DivRingOps -> R e. PrRing )
Theorem	isdmn 32207	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. Dmn <-> ( R e. PrRing /\ R e. Com2 ) )
Theorem	isdmn2 32208	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( R e. Dmn <-> ( R e. PrRing /\ R e. CRingOps ) )
Theorem	dmncrng 32209	A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. Dmn -> R e. CRingOps )
Theorem	dmnrngo 32210	A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- ( R e. Dmn -> R e. RingOps )
Theorem	flddmn 32211	A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( K e. Fld -> K e. Dmn )
21.18.19  Ideal generators
Syntax	cigen 32212	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 32213*	Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- IdlGen = ( r e. RingOps , s e. ~P ran ( 1st ` r ) |-> |^| { j e. ( Idl ` r ) | s C_ j } )
Theorem	igenval 32214*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) = |^| { j e. ( Idl ` R ) | S C_ j } )
Theorem	igenss 32215	A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> S C_ ( R IdlGen S ) )
Theorem	igenidl 32216	The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( R IdlGen S ) e. ( Idl ` R ) )
Theorem	igenmin 32217	The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) /\ S C_ I ) -> ( R IdlGen S ) C_ I )
Theorem	igenidl2 32218	The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> ( R IdlGen I ) = I )
Theorem	igenval2 32219*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ S C_ X ) -> ( ( R IdlGen S ) = I <-> ( I e. ( Idl ` R ) /\ S C_ I /\ A. j e. ( Idl ` R ) ( S C_ j -> I C_ j ) ) ) )
Theorem	prnc 32220*	A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. CRingOps /\ A e. X ) -> ( R IdlGen { A } ) = { x e. X | E. y e. X x = ( y H A ) } )
Theorem	isfldidl 32221	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- G = ( 1st ` K )   &    |- H = ( 2nd ` K )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( K e. Fld <-> ( K e. CRingOps /\ U =/= Z /\ ( Idl ` K ) = { { Z } , X } ) )
Theorem	isfldidl2 32222	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` K )   &    |- H = ( 2nd ` K )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( K e. Fld <-> ( K e. CRingOps /\ X =/= { Z } /\ ( Idl ` K ) = { { Z } , X } ) )
Theorem	ispridlc 32223*	The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. CRingOps -> ( P e. ( PrIdl ` R ) <-> ( P e. ( Idl ` R ) /\ P =/= X /\ A. a e. X A. b e. X ( ( a H b ) e. P -> ( a e. P \/ b e. P ) ) ) ) )
Theorem	pridlc 32224	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. X /\ B e. X /\ ( A H B ) e. P ) ) -> ( A e. P \/ B e. P ) )
Theorem	pridlc2 32225	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. X /\ ( A H B ) e. P ) ) -> B e. P )
Theorem	pridlc3 32226	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( ( R e. CRingOps /\ P e. ( PrIdl ` R ) ) /\ ( A e. ( X \ P ) /\ B e. ( X \ P ) ) ) -> ( A H B ) e. ( X \ P ) )
Theorem	isdmn3 32227*	The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   &    |- U = (GId ` H )   =>    |- ( R e. Dmn <-> ( R e. CRingOps /\ U =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )
Theorem	dmnnzd 32228	A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ ( A H B ) = Z ) ) -> ( A = Z \/ B = Z ) )
Theorem	dmncan1 32229	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H B ) = ( A H C ) -> B = C ) )
Theorem	dmncan2 32230	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   &    |- Z = (GId ` G )   =>    |- ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C =/= Z ) -> ( ( A H C ) = ( B H C ) -> A = B ) )
21.19  Mathbox for Giovanni Mascellani
21.19.1  Tools for automatic proof building The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings.
Theorem	efald2 32231	A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( -. ph -> F. )   =>    |- ph
Theorem	notbinot1 32232	Simplification rule of negation across a biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( -. ( -. ph <-> ps ) <-> ( ph <-> ps ) )
Theorem	bicontr 32233	Biimplication of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ( -. ph <-> ph ) <-> F. )
Theorem	impor 32234	An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ( ph -> ( ps \/ ch ) ) <-> ( ( -. ph \/ ps ) \/ ch ) )
Theorem	orfa 32235	The falsum F. can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ( ph \/ F. ) <-> ph )
Theorem	notbinot2 32236	Commutation rule between negation and biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( -. ( ph <-> ps ) <-> ( -. ph <-> ps ) )
Theorem	biimpor 32237	A rewriting rule for biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ( ( ph <-> ps ) -> ch ) <-> ( ( -. ph <-> ps ) \/ ch ) )
Theorem	unitresl 32238	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> ( ps \/ ch ) )   &    |- ( ph -> -. ch )   =>    |- ( ph -> ps )
Theorem	unitresr 32239	A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> ( ps \/ ch ) )   &    |- ( ph -> -. ps )   =>    |- ( ph -> ch )
Theorem	orfa1 32240	Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> ps )   =>    |- ( ( ph \/ F. ) -> ps )
Theorem	orfa2 32241	Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> F. )   =>    |- ( ( ph \/ ps ) -> ps )
Theorem	bifald 32242	Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> -. ps )   =>    |- ( ph -> ( ps <-> F. ) )
Theorem	orsild 32243	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> -. ( ps \/ ch ) )   =>    |- ( ph -> -. ps )
Theorem	orsird 32244	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
|- ( ph -> -. ( ps \/ ch ) )   =>    |- ( ph -> -. ch )
Theorem	orcomdd 32245	Commutativity of logic disjunction, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> ( ch \/ th ) ) )   =>    |- ( ph -> ( ps -> ( th \/ ch ) ) )
Theorem	cnf1dd 32246	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> -. ch ) )   &    |- ( ph -> ( ps -> ( ch \/ th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	cnf2dd 32247	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> -. th ) )   &    |- ( ph -> ( ps -> ( ch \/ th ) ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	cnfn1dd 32248	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> ( -. ch \/ th ) ) )   =>    |- ( ph -> ( ps -> th ) )
Theorem	cnfn2dd 32249	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ps -> ( ch \/ -. th ) ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	or32dd 32250	A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( ps -> ( ( ch \/ th ) \/ ta ) ) )   =>    |- ( ph -> ( ps -> ( ( ch \/ ta ) \/ th ) ) )
Theorem	notornotel1 32251	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> -. ( -. ps \/ ch ) )   =>    |- ( ph -> ps )
Theorem	notornotel2 32252	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> -. ( ps \/ -. ch ) )   =>    |- ( ph -> ch )
Theorem	contrd 32253	A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
|- ( ph -> ( -. ps -> ch ) )   &    |- ( ph -> ( -. ps -> -. ch ) )   =>    |- ( ph -> ps )
Theorem	an12i 32254	An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.)
|- ( ph /\ ( ps /\ ch ) )   =>    |- ( ps /\ ( ph /\ ch ) )
Theorem	exmid2 32255	An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ( ps /\ ph ) -> ch )   &    |- ( ( -. ps /\ et ) -> ch )   =>    |- ( ( ph /\ et ) -> ch )
Theorem	selconj 32256	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ( et /\ ph ) <-> ( ps /\ ( et /\ ch ) ) )
Theorem	truconj 32257	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ph <-> ( T. /\ ph ) )
Theorem	mergeconj 32258	An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ( et /\ ph ) <-> ( ( et /\ ps ) /\ ch ) )
Theorem	orel 32259	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ( ps /\ et ) -> th )   &    |- ( ( ch /\ rh ) -> th )   &    |- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ ( et /\ rh ) ) -> th )
Theorem	negel 32260	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ps -> ch )   &    |- ( ph -> -. ch )   =>    |- ( ( ph /\ ps ) -> F. )
Theorem	botel 32261	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ph -> F. )   =>    |- ( ph -> ps )
Theorem	tradd 32262	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ph <-> ps )   =>    |- ( ph <-> ( T. /\ ps ) )
Theorem	sbtru 32263	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. T. <-> T. )
Theorem	sbfal 32264	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. F. <-> F. )
Theorem	sbcani 32265	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph /\ ps ) <-> ( ch /\ et ) )
Theorem	sbcori 32266	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph \/ ps ) <-> ( ch \/ et ) )
Theorem	sbcimi 32267	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph -> ps ) <-> ( ch -> et ) )
Theorem	sbceqi 32268	Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- [_ A / x ]_ B = D   &    |- [_ A / x ]_ C = E   =>    |- ( [. A / x ]. B = C <-> D = E )
Theorem	sbcni 32269	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. -. ph <-> -. ps )
Theorem	sbali 32270	Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. A. x ph <-> A. x ph )
Theorem	sbexi 32271	Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. E. x ph <-> E. x ph )
Theorem	sbcalf 32272*	Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
|- F/_ y A   =>    |- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )
Theorem	sbcexf 32273*	Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
|- F/_ y A   =>    |- ( [. A / x ]. E. y ph <-> E. y [. A / x ]. ph )
Theorem	sbcalfi 32274*	Move universal quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/_ y A   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. A. y ph <-> A. y ps )
Theorem	sbcexfi 32275*	Move existential quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/_ y A   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. E. y ph <-> E. y ps )
Theorem	csbvargi 32276	The proper substitution of a class for a variable in that variable results in the class (if the class exists), in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   =>    |- [_ A / x ]_ x = A
Theorem	csbconstgi 32277*	The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   =>    |- [_ A / x ]_ y = y
Theorem	spsbcdi 32278	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   &    |- ( ph -> A. x ch )   &    |- ( [. A / x ]. ch <-> ps )   =>    |- ( ph -> ps )
Theorem	alrimii 32279*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/ y ph   &    |- ( ph -> ps )   &    |- ( [. y / x ]. ch <-> ps )   &    |- F/ y ch   =>    |- ( ph -> A. x ch )
Theorem	spesbcdi 32280	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- ( ph -> ps )   &    |- ( [. A / x ]. ch <-> ps )   =>    |- ( ph -> E. x ch )
Theorem	exlimddvf 32281	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- ( ph -> E. x th )   &    |- F/ x ps   &    |- ( ( th /\ ps ) -> ch )   &    |- F/ x ch   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	exlimddvfi 32282	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- ( ph -> E. x th )   &    |- F/ y th   &    |- F/ y ps   &    |- ( [. y / x ]. th <-> et )   &    |- ( ( et /\ ps ) -> ch )   &    |- F/ y ch   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	sbceq1ddi 32283	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- ( ph -> A = B )   &    |- ( ps -> th )   &    |- ( [. A / x ]. ch <-> th )   &    |- ( [. B / x ]. ch <-> et )   =>    |- ( ( ph /\ ps ) -> et )
Theorem	sbccom2lem 32284*	Lemma for sbccom2 32285. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2 32285*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2f 32286*	Commutative law for double class substitution, with non free variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   &    |- F/_ y A   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2fi 32287*	Commutative law for double class substitution, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
|- A e. _V   &    |- F/_ y A   &    |- [_ A / x ]_ B = C   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ps )
Theorem	sbcgfi 32288	Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
|- A e. _V   &    |- F/ x ph   =>    |- ( [. A / x ]. ph <-> ph )
Theorem	csbcom2fi 32289*	Commutative law for double class substitution in a class, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
|- A e. _V   &    |- F/_ y A   &    |- [_ A / x ]_ B = C   &    |- [_ A / x ]_ D = E   =>    |- [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ E
Theorem	csbgfi 32290	Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
|- A e. _V   &    |- F/_ x B   =>    |- [_ A / x ]_ B = B
21.19.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 32291	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> -. F. )
Theorem	tsim1 32292	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph -> ps ) ) )
Theorem	tsim2 32293	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ph \/ ( ph -> ps ) ) )
Theorem	tsim3 32294	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( -. ps \/ ( ph -> ps ) ) )
Theorem	tsbi1 32295	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ ( ph <-> ps ) ) )
Theorem	tsbi2 32296	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ ps ) \/ ( ph <-> ps ) ) )
Theorem	tsbi3 32297	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ -. ps ) \/ -. ( ph <-> ps ) ) )
Theorem	tsbi4 32298	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) )
Theorem	tsxo1 32299	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ -. ( ph \/_ ps ) ) )
Theorem	tsxo2 32300	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ ps ) \/ -. ( ph \/_ ps ) ) )