P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cdmn 35801	Extend class notation with the class of domains.
class Dmn
Definition	df-prrngo 35802	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 = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)}
Definition	df-dmn 35803	Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ Dmn = (PrRing ∩ Com2)
Theorem	isprrngo 35804	The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅)))
Theorem	prrngorngo 35805	A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps)
Theorem	smprngopr 35806	A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing)
Theorem	divrngpr 35807	A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing)
Theorem	isdmn 35808	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2))
Theorem	isdmn2 35809	The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps))
Theorem	dmncrng 35810	A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps)
Theorem	dmnrngo 35811	A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps)
Theorem	flddmn 35812	A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn)
20.20.22  Ideal generators
Syntax	cigen 35813	Extend class notation with the ideal generation function.
class IdlGen
Definition	df-igen 35814*	Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗})
Theorem	igenval 35815*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗})
Theorem	igenss 35816	A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆))
Theorem	igenidl 35817	The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅))
Theorem	igenmin 35818	The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼)
Theorem	igenidl2 35819	The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼)
Theorem	igenval2 35820*	The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗))))
Theorem	prnc 35821*	A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)})
Theorem	isfldidl 35822	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	isfldidl2 35823	Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝐾)    &   ⊢ 𝐻 = (2nd ‘𝐾)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑋 ≠ {𝑍} ∧ (Idl‘𝐾) = {{𝑍}, 𝑋}))
Theorem	ispridlc 35824*	The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
Theorem	pridlc 35825	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃))
Theorem	pridlc2 35826	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃)
Theorem	pridlc3 35827	Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃))
Theorem	isdmn3 35828*	The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    &   ⊢ 𝑈 = (GId‘𝐻)    ⇒   ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍))))
Theorem	dmnnzd 35829	A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍))
Theorem	dmncan1 35830	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶))
Theorem	dmncan2 35831	Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)
⊢ 𝐺 = (1st ‘𝑅)    &   ⊢ 𝐻 = (2nd ‘𝑅)    &   ⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑍 = (GId‘𝐺)    ⇒   ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐶 ≠ 𝑍) → ((𝐴𝐻𝐶) = (𝐵𝐻𝐶) → 𝐴 = 𝐵))
20.21  Mathbox for Giovanni Mascellani
20.21.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 35832	A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ 𝜑 → ⊥)    ⇒   ⊢ 𝜑
Theorem	notbinot1 35833	Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓))
Theorem	bicontr 35834	Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥)
Theorem	impor 35835	An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	orfa 35836	The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑)
Theorem	notbinot2 35837	Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓))
Theorem	biimpor 35838	A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒))
Theorem	orfa1 35839	Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ ⊥) → 𝜓)
Theorem	orfa2 35840	Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ ((𝜑 ∨ 𝜓) → 𝜓)
Theorem	bifald 35841	Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ ⊥))
Theorem	orsild 35842	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	orsird 35843	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	cnf1dd 35844	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnf2dd 35845	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ¬ 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	cnfn1dd 35846	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	cnfn2dd 35847	A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	or32dd 35848	A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃)))
Theorem	notornotel1 35849	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	notornotel2 35850	A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	contrd 35851	A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.)
⊢ (𝜑 → (¬ 𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	an12i 35852	An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.)
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒))
Theorem	exmid2 35853	An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ ((𝜓 ∧ 𝜑) → 𝜒)    &   ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜂) → 𝜒)
Theorem	selconj 35854	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒)))
Theorem	truconj 35855	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (⊤ ∧ 𝜑))
Theorem	orel 35856	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ ((𝜓 ∧ 𝜂) → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜌) → 𝜃)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃)
Theorem	negel 35857	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 → ¬ 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ⊥)
Theorem	botel 35858	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 → ⊥)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	tradd 35859	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ (⊤ ∧ 𝜓))
Theorem	gm-sbtru 35860	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤)
Theorem	sbfal 35861	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥)
Theorem	sbcani 35862	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂))
Theorem	sbcori 35863	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂))
Theorem	sbcimi 35864	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂)    ⇒   ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂))
Theorem	sbcni 35865	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓)
Theorem	sbali 35866	Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbexi 35867	Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑)
Theorem	sbcalf 35868*	Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcexf 35869*	Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑)
Theorem	sbcalfi 35870*	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.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓)
Theorem	sbcexfi 35871*	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.)
⊢ Ⅎ𝑦𝐴    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓)
Theorem	spsbcdi 35872	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ (𝜑 → ∀𝑥𝜒)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	alrimii 35873*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → 𝜓)    &   ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ (𝜑 → ∀𝑥𝜒)
Theorem	spesbcdi 35874	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥𝜒)
Theorem	exlimddvf 35875	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑥𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	exlimddvfi 35876	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → ∃𝑥𝜃)    &   ⊢ Ⅎ𝑦𝜃    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂)    &   ⊢ ((𝜂 ∧ 𝜓) → 𝜒)    &   ⊢ Ⅎ𝑦𝜒    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	sbceq1ddi 35877	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ (𝜑 → 𝐴 = 𝐵)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃)    &   ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	sbccom2lem 35878*	Lemma for sbccom2 35879. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2 35879*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2f 35880*	Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑)
Theorem	sbccom2fi 35881*	Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓)
Theorem	csbcom2fi 35882*	Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
⊢ 𝐴 ∈ V    &   ⊢ Ⅎ𝑦𝐴    &   ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶    &   ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸    ⇒   ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸
20.21.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 35883	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ¬ ⊥)
Theorem	tsim1 35884	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓)))
Theorem	tsim2 35885	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓)))
Theorem	tsim3 35886	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓)))
Theorem	tsbi1 35887	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi2 35888	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓)))
Theorem	tsbi3 35889	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsbi4 35890	A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
Theorem	tsxo1 35891	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo2 35892	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓)))
Theorem	tsxo3 35893	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsxo4 35894	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓)))
Theorem	tsan1 35895	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))
Theorem	tsan2 35896	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsan3 35897	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ ¬ (𝜑 ∧ 𝜓)))
Theorem	tsna1 35898	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊼ 𝜓)))
Theorem	tsna2 35899	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜑 ∨ (𝜑 ⊼ 𝜓)))
Theorem	tsna3 35900	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
⊢ (𝜃 → (𝜓 ∨ (𝜑 ⊼ 𝜓)))