P. 482 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48101-48200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wrddin 48101	A word in two alphabets is also a word under their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶) → 𝐴 ∈ Word (𝐵 ∩ 𝐶))
Theorem	wrddrin 48102	A word whose alphabet is intersection of two classes is also a word in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ Word (𝐵 ∩ 𝐶) → (𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶))
Theorem	wrddin2 48103	Distribution of word class constructor over class intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ Word (𝐵 ∩ 𝐶) = (Word 𝐵 ∩ Word 𝐶)
Theorem	wrddun 48104	Words in either of two alphabets are words in their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ Word 𝐵 ∨ 𝐴 ∈ Word 𝐶) → 𝐴 ∈ Word (𝐵 ∪ 𝐶))
Theorem	wrddun2 48105	Superadditivity of word constructor. Class of words over union alphabet includes all words over either alphabet in the union; if 𝐵 and 𝐶 are non-empty and different, then this subclass relation is strict because of the words which have symbols both from 𝐵 and from 𝐶. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (Word 𝐵 ∪ Word 𝐶) ⊆ Word (𝐵 ∪ 𝐶)
Theorem	chndin 48106	A chain in two alphabets at once is also a chain in their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ (𝑅 Chain 𝐶)) → 𝐴 ∈ (𝑅 Chain (𝐵 ∩ 𝐶)))
Theorem	chndrin 48107	A chain whose alphabet is intersection of two classes is also a chain in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ (𝑅 Chain (𝐵 ∩ 𝐶)) → (𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ (𝑅 Chain 𝐶)))
Theorem	chndin2 48108	Distribution of chain class constructor over alphabet intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝑅 Chain (𝐵 ∩ 𝐶)) = ((𝑅 Chain 𝐵) ∩ (𝑅 Chain 𝐶))
Theorem	chndun 48109	Chains in either of two alphabets are chains in their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∨ 𝐴 ∈ (𝑅 Chain 𝐶)) → 𝐴 ∈ (𝑅 Chain (𝐵 ∪ 𝐶)))
Theorem	chndun2 48110	Superaddivity of chain constructor over alphabet parameter. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 Chain 𝐵) ∪ (𝑅 Chain 𝐶)) ⊆ (𝑅 Chain (𝐵 ∪ 𝐶))
Theorem	chnrin 48111	Satisfying two chain relations makes a chain under their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ ( < Chain 𝐵)) → 𝐴 ∈ ((𝑅 ∩ < ) Chain 𝐵))
Theorem	chnrrin 48112	A chain of elements satisfying two relations at once is a chain under either of them. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ ((𝑅 ∩ < ) Chain 𝐵) → (𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ ( < Chain 𝐵)))
Theorem	chnrin2 48113	Distribution of chain class constructor over relation intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 ∩ < ) Chain 𝐵) = ((𝑅 Chain 𝐵) ∩ ( < Chain 𝐵))
Theorem	chnrun 48114	Satisfying either of two chain relations is sufficient to make a chain under their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∨ 𝐴 ∈ ( < Chain 𝐵)) → 𝐴 ∈ ((𝑅 ∪ < ) Chain 𝐵))
Theorem	chnrun2 48115	Superadditivity of chain constructor over relation parameter. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 Chain 𝐵) ∪ ( < Chain 𝐵)) ⊆ ((𝑅 ∪ < ) Chain 𝐵)
21.49.3  Scratchpad for number theory
Theorem	evenwodadd 48116	If an integer is multiplied by its sum with an odd number (thus changing its parity), the result is even. (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝐼 ∈ ℤ)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐽)    ⇒   ⊢ (𝜑 → 2 ∥ (𝐼 · (𝐼 + 𝐽)))
21.49.4  Scratchpad for math on real numbers
Theorem	squeezedltsq 48117	If a real value is squeezed between two others, its square is less than square of at least one of them. Deduction form. (Contributed by Ender Ting, 31-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐵) < (𝐴 · 𝐴) ∨ (𝐵 · 𝐵) < (𝐶 · 𝐶)))
Theorem	sqrtnnaa 48118	Square root of a natural number is algebraic. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ (𝐴 ∈ ℕ → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtnzqaa 48119	Square root of a nonzero rational is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtqaa 48120	Square root of a rational number is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ (𝐴 ∈ ℚ → (√‘𝐴) ∈ 𝔸)
Theorem	numtowerdt 48121	Certain number sets and fields form a tower. In particular, singleton 1, natural numbers, natural numbers with zero, integers, rationals, algebraic reals (notice that current definition allows algebraic numbers to be complex thus the restriction), reals and complex number sets are a tower of proper subsets. (Contributed by Ender Ting, 31-Jul-2026.)
⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( [⊊] Chain V)
Theorem	sin3t 48122	Triple-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝐴 ∈ ℂ → (sin‘(3 · 𝐴)) = ((3 · (sin‘𝐴)) − (4 · ((sin‘𝐴)↑3))))
Theorem	cos3t 48123	Triple-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))
Theorem	sin5tlem1 48124	Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝑁 ∈ ℂ → (((3 · 𝑁) − (4 · (𝑁↑3))) · (1 − (2 · (𝑁↑2)))) = (((8 · (𝑁↑5)) − (;10 · (𝑁↑3))) + (3 · 𝑁)))
Theorem	sin5tlem2 48125	Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · 𝑁) = ((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2)))))
Theorem	sin5tlem3 48126	Lemma 3 for quintupled angle sine calculation, multiplicating triple angle cosine by double angle sine. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = (((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2)))) · (2 · 𝑀)))
Theorem	sin5tlem4 48127	Lemma 4 for quintupled angle sine calculation: expanding lemma 3 result to difference of polynomials. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))))
Theorem	sin5tlem5 48128	Lemma 5 for quintupled angle sine calculation: sine of triple-angle and double-angle sum, as a polynomial in sine straight. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))
Theorem	sin5t 48129	Five-times-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ (𝐴 ∈ ℂ → (sin‘(5 · 𝐴)) = (((;16 · ((sin‘𝐴)↑5)) − (;20 · ((sin‘𝐴)↑3))) + (5 · (sin‘𝐴))))
Theorem	cos5t 48130	Five-times-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 20-Apr-2026.)
⊢ (𝐴 ∈ ℂ → (cos‘(5 · 𝐴)) = (((;16 · ((cos‘𝐴)↑5)) − (;20 · ((cos‘𝐴)↑3))) + (5 · (cos‘𝐴))))
Theorem	cos5teq 48131	Five-times-angle formula for cosine, substitution helper. (Contributed by Ender Ting, 9-May-2026.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 = (5 · 𝐴) ∧ 𝐶 = (cos‘𝐴)) → (cos‘𝐵) = (((;16 · (𝐶↑5)) − (;20 · (𝐶↑3))) + (5 · 𝐶)))
Theorem	goldpolyfactor 48132	Factorization of a polynomial which has golden ratio among its roots, done by term-by-term-by-term multiplying and summing a few shorter polynomials. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 ∈ ℂ    ⇒   ⊢ (((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) · (𝐹 + 2)) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)
Theorem	goldrarr 48133	The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ
Theorem	goldrasin 48134	Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = (2 · (sin‘(π · (3 / ;10))))
Theorem	goldrapos 48135	Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 0 < 𝐹
Theorem	goldrarp 48136	The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ+
Theorem	goldracos5teq 48137	Lemma 1 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ (cos‘π) = (((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) + (5 · (𝐹 / 2)))
Theorem	goldratmolem2 48138	Lemma 2 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ -1 = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2)))
Theorem	goldratmolem3 48139	Lemma 3 for determining the value of golden ratio. (Contributed by Ender Ting, 23-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2) = 0
Theorem	goldratmolem4 48140	Lemma 4 for determining the value of golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ (((𝐹↑2) − 𝐹) − 1) = 0
Theorem	goldratval 48141	Value of the golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = ((1 + (√‘5)) / 2)
Theorem	lambert0 48142	A value of Lambert W (product logarithm) function at zero. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ 0𝑅0
Theorem	lamberte 48143	A value of Lambert W (product logarithm) function at e. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ e𝑅1
Theorem	cjnpoly 48144	Complex conjugation operator is not a polynomial with complex coefficients. Indeed; if it was, then multiplying 𝑥 conjugate by 𝑥 itself and adding 1 would yield a nowhere-zero non-constant polynomial, contrary to the fta 27437. (Contributed by Ender Ting, 8-Dec-2025.)
⊢ ¬ ∗ ∈ (Poly‘ℂ)
Theorem	tannpoly 48145	The tangent function is not a polynomial with complex coefficients, as it is not defined on the whole complex plane. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ tan ∈ (Poly‘ℂ)
Theorem	sinnpoly 48146	Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 26659. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ sin ∈ (Poly‘ℂ)
Theorem	sqrtrrnpoly 48147	Real square root is not a polynomial with real coefficients, because its value is imaginary for negative arguments. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ¬ √ ∈ (Poly‘ℝ)
Theorem	sqrtnpoly 48148	Square root function is not polynomial with complex coefficients either. Otherwise, its composition with a square monomial - the identity - would have to be of even degree. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ¬ √ ∈ (Poly‘ℂ)
21.49.5  Turing Machine Finite Reach theorem
Theorem	tmachlem-extapes 48149*	The class of all tapes is a set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → 𝑇 ∈ V)
Theorem	tmachlem-finscan 48150*	Execution on any tape only scanned a finite number of cells. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝑆‘𝑎) ∈ Fin)
Theorem	tmachlem-agreeself 48151*	Any tape belongs to its own agreement set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ∈ (𝐴‘𝑎))
Theorem	tmachlem-agreeprod 48152*	Agreement set can be written as infinite product of acceptable values for tape's cells. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝐴‘𝑎) = X𝑖 ∈ 𝐼 if(𝑖 ∈ (𝑆‘𝑎), {(𝑎‘𝑖)}, 𝑈))
Theorem	tmachlem-tpcomp 48153*	Product (discrete) topology of tapes is compact by Tychonoff's theorem. To work for infinite index sets (such as ℤ for 𝐼 which is the main interpretation), it requires Choice. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) ∈ Comp)
Theorem	tmachlem-tpbase 48154*	The base set of product topology of tapes is the set of tapes. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) = 𝑇)
Theorem	tmachlem-tpitem 48155*	Topology lemma. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)‘𝑎) = 𝒫 𝑈)
Theorem	tmachlem-tpopen 48156*	Agreement sets are open in the product topology of tapes. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → X𝑏 ∈ 𝐼 if(𝑏 ∈ (𝑆‘𝑎), {(𝑎‘𝑏)}, 𝑈) ∈ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)))
Theorem	tmachlem-tpopen2 48157*	Variable-renaming lemma connecting tmachlem-agreeprod 48152 and tmachlem-tpopen 48156. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝐴‘𝑎) ∈ (∏t‘(𝑏 ∈ 𝐼 ↦ 𝒫 𝑈)))
Theorem	tmachlem-uassst 48158*	Union of all agreement sets only includes tapes. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑇)
Theorem	tmachlem-exlargecover 48159*	Product topology of tapes has an open cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 = 𝑇)
Theorem	tmachlem-extpcover 48160*	Product topology of tapes admits finite cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝒫 ran 𝐴 ∩ Fin)∪ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) = ∪ 𝑎)
Theorem	tmachlem-exagreecover 48161*	Particular properties of the finite cover of agreesets. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎(𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎))
Theorem	tmachlem-agreesn 48162*	Scans for all tapes of a single agreement set are identical. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝑆 “ (𝐴‘𝑎)) = {(𝑆‘𝑎)})
Theorem	tmachlem-agreefin 48163*	Any agreement set has a finite (singleton) list of possible scans. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑏 ∈ ran 𝐴) → (𝑆 “ 𝑏) ∈ Fin)
Theorem	tmachlem-franscan 48164*	There is a finite number of different scan sets. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ran 𝑆 ∈ Fin)
Theorem	tmachlem-fssscan 48165*	Any scan set is finite. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ran 𝑆 ⊆ Fin)
Theorem	tmachfullfin 48166*	Folk theorem. For any algorithm deterministically processing a stream of data (essentially, an infinite tape with cell indices 𝐼 and finite alphabet 𝑈), if it terminates on every possible input, then it never looks beyond a finite portion ∪ ran 𝑆 of the input. Termination is expressed here with a weaker condition: that an execution may only look at a finite number of cells. Obviously, a program which finishes in a finite number of steps can only scan finite set of cells. This theorem has many corollaries, such as: any encoding scheme able to represent all integers has at least one non-decodable tape (in other terms, encoding of the infinity). I no longer have the source for this theorem but I believe I first read about it on LessWrong. My gratitude to Grok for suggesting that this theorem will require Axiom of Choice, and to DeepSeek for suggesting the topology-based proof route. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝑆 ∈ Fin)
21.50  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 48167	The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑))
Theorem	ax3h 48168	Recover ax-3 8 from hirstL-ax3 48167. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	aibandbiaiffaiffb 48169	A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓))
Theorem	aibandbiaiaiffb 48170	A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
Theorem	notatnand 48171	Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	aistia 48172	Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    ⇒   ⊢ 𝜑
Theorem	aisfina 48173	Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    ⇒   ⊢ ¬ 𝜑
Theorem	bothtbothsame 48174	Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	bothfbothsame 48175	Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	aiffbbtat 48176	Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	aisbbisfaisf 48177	Given a is equivalent to b, b is equivalent to ⊥ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	axorbtnotaiffb 48178	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1542 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 48179	Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ ¬ (𝜒 ↔ 𝜓)
Theorem	axorbciffatcxorb 48180	Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ (𝜒 ⊻ 𝜓)
Theorem	aibnbna 48181	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 48182	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 48183	Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (⊤ ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	astbstanbst 48184	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ⊤)
Theorem	aistbistaandb 48185	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	aisbnaxb 48186	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 48187	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 48188	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 48189	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 48190	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 48191	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 48192	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	conimpfalt 48193	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aistbisfiaxb 48194	Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aisfbistiaxb 48195	Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aifftbifffaibif 48196	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 → 𝜓) ↔ ⊥)
Theorem	aifftbifffaibifff 48197	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 ↔ 𝜓) ↔ ⊥)
Theorem	atnaiana 48198	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 48199	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 48200	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑