P. 481 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48001-48100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chnrrin 48001	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 48002	Distribution of chain class constructor over relation intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 ∩ < ) Chain 𝐵) = ((𝑅 Chain 𝐵) ∩ ( < Chain 𝐵))
Theorem	chnrun 48003	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 48004	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 48005	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 48006	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 48007	Square root of a natural number is algebraic. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ (𝐴 ∈ ℕ → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtnzqaa 48008	Square root of a nonzero rational is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtqaa 48009	Square root of a rational number is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ (𝐴 ∈ ℚ → (√‘𝐴) ∈ 𝔸)
Theorem	numtowerdt 48010	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 48011	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 48012	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 48013	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 48014	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 48015	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 48016	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 48017	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 48018	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 48019	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 48020	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 48021	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 48022	The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ
Theorem	goldrasin 48023	Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = (2 · (sin‘(π · (3 / ;10))))
Theorem	goldrapos 48024	Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 0 < 𝐹
Theorem	goldrarp 48025	The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ+
Theorem	goldracos5teq 48026	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 48027	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 48028	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 48029	Lemma 4 for determining the value of golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ (((𝐹↑2) − 𝐹) − 1) = 0
Theorem	goldratval 48030	Value of the golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = ((1 + (√‘5)) / 2)
Theorem	lambert0 48031	A value of Lambert W (product logarithm) function at zero. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ 0𝑅0
Theorem	lamberte 48032	A value of Lambert W (product logarithm) function at e. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ e𝑅1
Theorem	cjnpoly 48033	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 27413. (Contributed by Ender Ting, 8-Dec-2025.)
⊢ ¬ ∗ ∈ (Poly‘ℂ)
Theorem	tannpoly 48034	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 48035	Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 26635. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ sin ∈ (Poly‘ℂ)
Theorem	sqrtrrnpoly 48036	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 48037	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 48038*	The class of all tapes is a set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → 𝑇 ∈ V)
Theorem	tmachlem-finscan 48039*	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 48040*	Any tape belongs to its own agreement set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ∈ (𝐴‘𝑎))
Theorem	tmachlem-agreeprod 48041*	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 48042*	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 48043*	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 48044*	Topology lemma. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)‘𝑎) = 𝒫 𝑈)
Theorem	tmachlem-tpopen 48045*	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 48046*	Variable-renaming lemma connecting tmachlem-agreeprod 48041 and tmachlem-tpopen 48045. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝐴‘𝑎) ∈ (∏t‘(𝑏 ∈ 𝐼 ↦ 𝒫 𝑈)))
Theorem	tmachlem-uassst 48047*	Union of all agreement sets only includes tapes. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑇)
Theorem	tmachlem-exlargecover 48048*	Product topology of tapes has an open cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 = 𝑇)
Theorem	tmachlem-extpcover 48049*	Product topology of tapes admits finite cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝒫 ran 𝐴 ∩ Fin)∪ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) = ∪ 𝑎)
Theorem	tmachlem-exagreecover 48050*	Particular properties of the finite cover of agreesets. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎(𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎))
Theorem	tmachlem-agreesn 48051*	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 48052*	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 48053*	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 48054*	Any scan set is finite. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ran 𝑆 ⊆ Fin)
Theorem	tmachfullfin 48055*	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 48056	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 48057	Recover ax-3 8 from hirstL-ax3 48056. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	aibandbiaiffaiffb 48058	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 48059	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 48060	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 48061	Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    ⇒   ⊢ 𝜑
Theorem	aisfina 48062	Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    ⇒   ⊢ ¬ 𝜑
Theorem	bothtbothsame 48063	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 48064	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 48065	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 48066	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 48067	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1541 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 48068	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 48069	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 48070	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 48071	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 48072	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 48073	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 48074	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 48075	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 48076	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 48077	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 48078	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 48079	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 48080	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 48081	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 48082	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 48083	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 48084	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 48085	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 48086	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 48087	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 48088	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 48089	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 48090	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 48091	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 48092	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 48093	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	abciffcbatnabciffncbai 48094	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	nabctnabc 48095	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒))
Theorem	jabtaib 48096	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	onenotinotbothi 48097	From one negated implication it is not the case its nonnegated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ ¬ (𝜑 → 𝜓)    ⇒   ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃))
Theorem	twonotinotbothi 48098	From these two negated implications it is not the case their nonnegated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ ¬ (𝜑 → 𝜓)    &   ⊢ ¬ (𝜒 → 𝜃)    ⇒   ⊢ ¬ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜃))
Theorem	clifte 48099	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ ¬ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftet 48100	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))