P. 474 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47301-47400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	et-sqrtnegnre 47301	The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → ¬ (√‘𝐴) ∈ ℝ)
Theorem	ormklocald 47302*	If elements of a certain sequence are ordered with respect to a certain relation, then its consecutive elements satisfy that relation (so-called "local monotonicity"). (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝑅 Or 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(𝑇 + 1))(𝐵‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘)𝑅(𝐵‘𝑡)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘)𝑅(𝐵‘(𝑘 + 1)))
Theorem	ormkglobd 47303*	If all adjacent elements of a certain sequence are ordered according to a relation which is a total order on S, then any element is so related to anything to right of it (so-called "global monotonicity"). Deduction form. (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝑅 Or 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(𝑇 + 1))(𝐵‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘)𝑅(𝐵‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘)𝑅(𝐵‘𝑡)))
Theorem	natlocalincr 47304*	Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024.)
⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘) < (𝐵‘𝑡))    ⇒   ⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1))
Theorem	natglobalincr 47305*	Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.)
⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1))    &   ⊢ 𝑇 ∈ ℤ    ⇒   ⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵‘𝑘) < (𝐵‘𝑡)
Theorem	chnsubseqword 47306	A subsequence of a chain is a word. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ Word 𝐴)
Theorem	chnsubseqwl 47307	A subsequence of a chain has the same length as its indexing sequence. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    ⇒   ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) = (♯‘𝐼))
Theorem	chnsubseq 47308	An order-preserving subsequence of an ordered chain is itself a chain. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    &   ⊢ (𝜑 → < Po 𝐴)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ ( < Chain 𝐴))
Theorem	chnsuslle 47309	Length of a subsequence is bounded by the length of original chain. (Contributed by Ender Ting, 30-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    &   ⊢ (𝜑 → < Po 𝐴)    ⇒   ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) ≤ (♯‘𝑊))
Theorem	chnerlem1 47310	In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub 18588 to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐽) ∼ (lastS‘𝐶))
Theorem	chnerlem2 47311	Lemma for chner 47313 where the I-th element comes before the J-th. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝐽)) → (𝐶‘𝐼) ∼ (𝐶‘𝐽))
Theorem	chnerlem3 47312	Lemma for chner 47313- trichotomy of integers within the word's domain. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐼 ∈ (0..^𝐽) ∨ 𝐽 ∈ (0..^𝐼) ∨ 𝐼 = 𝐽))
Theorem	chner 47313	Any two elements are equivalent in a chain constructed on an equivalence relation. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) ∼ (𝐶‘𝐽))
Theorem	nthrucw 47314*	Some number sets form a chain of proper subsets. This is rephrasing nthruc 16219 as a statement about chains; the hypothesis sets the ordering relation to be "is a proper subset". The theorem talks about singleton 1, natural numbers, natural-or-zero numbers, integers, rational numbers, algebraic reals (the definition includes complex numbers as algebraic so intersection is taken), real numbers and complex numbers, which are proper subsets in order. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ < = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}    ⇒   ⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( < Chain V)
21.45.2  Scratchpad for number theory
Theorem	evenwodadd 47315	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.45.3  Scratchpad for math on real numbers
Theorem	squeezedltsq 47316	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	sin3t 47317	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 47318	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 47319	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 47320	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 47321	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 47322	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 47323	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 47324	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	goldrarr 47325	The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ
Theorem	goldrasin 47326	Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = (2 · (sin‘(π · (3 / ;10))))
Theorem	goldrapos 47327	Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 0 < 𝐹
Theorem	goldrarp 47328	The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ+
Theorem	lambert0 47329	A value of Lambert W (product logarithm) function at zero. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ 0𝑅0
Theorem	lamberte 47330	A value of Lambert W (product logarithm) function at e. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ e𝑅1
Theorem	cjnpoly 47331	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 27043. (Contributed by Ender Ting, 8-Dec-2025.)
⊢ ¬ ∗ ∈ (Poly‘ℂ)
Theorem	tannpoly 47332	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 47333	Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 26274. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ sin ∈ (Poly‘ℂ)
21.46  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 47334	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 47335	Recover ax-3 8 from hirstL-ax3 47334. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	aibandbiaiffaiffb 47336	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 47337	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 47338	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 47339	Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    ⇒   ⊢ 𝜑
Theorem	aisfina 47340	Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    ⇒   ⊢ ¬ 𝜑
Theorem	bothtbothsame 47341	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 47342	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 47343	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 47344	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 47345	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1514 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 47346	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 47347	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 47348	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 47349	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 47350	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 47351	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 47352	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 47353	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 47354	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 47355	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 47356	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 47357	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 47358	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 47359	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 47360	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 47361	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 47362	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 47363	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 47364	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 47365	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 47366	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 47367	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 47368	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 47369	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 47370	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 47371	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 47372	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	nabctnabc 47373	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒))
Theorem	jabtaib 47374	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	onenotinotbothi 47375	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 47376	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 47377	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ ¬ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftet 47378	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	clifteta 47379	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftetb 47380	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	confun 47381	Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜃 ↔ 𝜑))
Theorem	confun2 47382	Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)))    &   ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑))    ⇒   ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑)))
Theorem	confun3 47383	Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜑 ↔ (𝜒 → 𝜓))    &   ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓))    ⇒   ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓)))
Theorem	confun4 47384	An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ ((𝜑 → 𝜓) → 𝜓)    &   ⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓))    &   ⊢ (𝜏 ↔ (𝜒 → 𝜃))    &   ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜒 → (𝜓 → 𝜏))
Theorem	confun5 47385	An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    &   ⊢ ((𝜑 → 𝜓) → 𝜓)    &   ⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓))    &   ⊢ (𝜏 ↔ (𝜒 → 𝜃))    &   ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜒 → (𝜂 ↔ 𝜏))
Theorem	plcofph 47386	Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜒
Theorem	pldofph 47387	Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    ⇒   ⊢ 𝜏
Theorem	plvcofph 47388	Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    ⇒   ⊢ 𝜂
Theorem	plvcofphax 47389	Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    &   ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏))    ⇒   ⊢ 𝜁
Theorem	plvofpos 47390	rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))    &   ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂))))    &   ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂))))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎))    &   ⊢ 𝜁    &   ⊢ 𝜎    ⇒   ⊢ 𝜌
Theorem	mdandyv0 47391	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊥)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv1 47392	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊤)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv2 47393	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊥)    &   ⊢ (𝜃 ↔ ⊤)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv3 47394	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊤)    &   ⊢ (𝜃 ↔ ⊤)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv4 47395	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊥)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊤)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv5 47396	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊤)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊤)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv6 47397	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊥)    &   ⊢ (𝜃 ↔ ⊤)    &   ⊢ (𝜏 ↔ ⊤)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv7 47398	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊤)    &   ⊢ (𝜃 ↔ ⊤)    &   ⊢ (𝜏 ↔ ⊤)    &   ⊢ (𝜂 ↔ ⊥)    ⇒   ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜓)) ∧ (𝜏 ↔ 𝜓)) ∧ (𝜂 ↔ 𝜑))
Theorem	mdandyv8 47399	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊥)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊤)    ⇒   ⊢ ((((𝜒 ↔ 𝜑) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓))
Theorem	mdandyv9 47400	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    &   ⊢ (𝜒 ↔ ⊤)    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊤)    ⇒   ⊢ ((((𝜒 ↔ 𝜓) ∧ (𝜃 ↔ 𝜑)) ∧ (𝜏 ↔ 𝜑)) ∧ (𝜂 ↔ 𝜓))