P. 445 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44401-44500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	aibnbna 44401	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 44402	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 44403	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 44404	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 44405	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 44406	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 44407	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 44408	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 44409	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 44410	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 44411	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 44412	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 44413	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 44414	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 44415	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 44416	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 44417	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 44418	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 44419	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 44420	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 44421	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 44422	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 44423	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 44424	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 44425	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	nabctnabc 44426	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒))
Theorem	jabtaib 44427	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	onenotinotbothi 44428	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 44429	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 44430	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ ¬ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftet 44431	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	clifteta 44432	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftetb 44433	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	confun 44434	Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜃 ↔ 𝜑))
Theorem	confun2 44435	Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)))    &   ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑))    ⇒   ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑)))
Theorem	confun3 44436	Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜑 ↔ (𝜒 → 𝜓))    &   ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓))    ⇒   ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓)))
Theorem	confun4 44437	An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ ((𝜑 → 𝜓) → 𝜓)    &   ⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓))    &   ⊢ (𝜏 ↔ (𝜒 → 𝜃))    &   ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜒 → (𝜓 → 𝜏))
Theorem	confun5 44438	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 44439	Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜒
Theorem	pldofph 44440	Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    ⇒   ⊢ 𝜏
Theorem	plvcofph 44441	Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    ⇒   ⊢ 𝜂
Theorem	plvcofphax 44442	Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    &   ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏))    ⇒   ⊢ 𝜁
Theorem	plvofpos 44443	rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))    &   ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂))))    &   ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂))))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎))    &   ⊢ 𝜁    &   ⊢ 𝜎    ⇒   ⊢ 𝜌
Theorem	mdandyv0 44444	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 44445	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 44446	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 44447	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 44448	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 44449	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 44450	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 44451	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 44452	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 44453	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	mdandyv10 44454	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	mdandyv11 44455	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	mdandyv12 44456	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	mdandyv13 44457	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	mdandyv14 44458	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	mdandyv15 44459	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	mdandyvr0 44460	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr1 44461	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr2 44462	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr3 44463	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr4 44464	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr5 44465	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr6 44466	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr7 44467	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜁))
Theorem	mdandyvr8 44468	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr9 44469	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr10 44470	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr11 44471	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜁)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr12 44472	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr13 44473	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜁)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr14 44474	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜁) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvr15 44475	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ 𝜁)    &   ⊢ (𝜓 ↔ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ↔ 𝜎) ∧ (𝜃 ↔ 𝜎)) ∧ (𝜏 ↔ 𝜎)) ∧ (𝜂 ↔ 𝜎))
Theorem	mdandyvrx0 44476	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx1 44477	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx2 44478	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx3 44479	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx4 44480	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx5 44481	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx6 44482	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx7 44483	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜑)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜁))
Theorem	mdandyvrx8 44484	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx9 44485	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx10 44486	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx11 44487	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜑)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜁)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx12 44488	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx13 44489	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜑)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜁)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx14 44490	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜁) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎))
Theorem	mdandyvrx15 44491	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜁)    &   ⊢ (𝜓 ⊻ 𝜎)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜓)    &   ⊢ (𝜂 ↔ 𝜓)    ⇒   ⊢ ((((𝜒 ⊻ 𝜎) ∧ (𝜃 ⊻ 𝜎)) ∧ (𝜏 ⊻ 𝜎)) ∧ (𝜂 ⊻ 𝜎))
Theorem	H15NH16TH15IH16 44492	Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ 𝜂    &   ⊢ 𝜁    &   ⊢ 𝜎    &   ⊢ 𝜌    &   ⊢ 𝜇    &   ⊢ 𝜆    &   ⊢ 𝜅    &   ⊢ jph    &   ⊢ jps    &   ⊢ jch    &   ⊢ jth    ⇒   ⊢ (((((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ jph) ∧ jps) ∧ jch) → jth)
Theorem	dandysum2p2e4 44493	CONTRADICTION PROVED AT 1 + 1 = 2 . Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2', 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (𝜑 ↔ (𝜃 ∧ 𝜏))    &   ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁))    &   ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌))    &   ⊢ (𝜃 ↔ ⊥)    &   ⊢ (𝜏 ↔ ⊥)    &   ⊢ (𝜂 ↔ ⊤)    &   ⊢ (𝜁 ↔ ⊤)    &   ⊢ (𝜎 ↔ ⊥)    &   ⊢ (𝜌 ↔ ⊥)    &   ⊢ (𝜇 ↔ ⊥)    &   ⊢ (𝜆 ↔ ⊥)    &   ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))    &   ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))    &   ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))    &   ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))    ⇒   ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))
Theorem	mdandysum2p2e4 44494	CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a successful version of his own. See Mario's Relevant Work: Half adder and full adder in propositional calculus. Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added would exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). E.g., 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.)
⊢ (jth ↔ ⊥)    &   ⊢ (jta ↔ ⊤)    &   ⊢ (𝜑 ↔ (𝜃 ∧ 𝜏))    &   ⊢ (𝜓 ↔ (𝜂 ∧ 𝜁))    &   ⊢ (𝜒 ↔ (𝜎 ∧ 𝜌))    &   ⊢ (𝜃 ↔ jth)    &   ⊢ (𝜏 ↔ jth)    &   ⊢ (𝜂 ↔ jta)    &   ⊢ (𝜁 ↔ jta)    &   ⊢ (𝜎 ↔ jth)    &   ⊢ (𝜌 ↔ jth)    &   ⊢ (𝜇 ↔ jth)    &   ⊢ (𝜆 ↔ jth)    &   ⊢ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))    &   ⊢ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))    &   ⊢ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))    &   ⊢ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))    ⇒   ⊢ ((((((((((((((((𝜑 ↔ (𝜃 ∧ 𝜏)) ∧ (𝜓 ↔ (𝜂 ∧ 𝜁))) ∧ (𝜒 ↔ (𝜎 ∧ 𝜌))) ∧ (𝜃 ↔ ⊥)) ∧ (𝜏 ↔ ⊥)) ∧ (𝜂 ↔ ⊤)) ∧ (𝜁 ↔ ⊤)) ∧ (𝜎 ↔ ⊥)) ∧ (𝜌 ↔ ⊥)) ∧ (𝜇 ↔ ⊥)) ∧ (𝜆 ↔ ⊥)) ∧ (𝜅 ↔ ((𝜃 ⊻ 𝜏) ⊻ (𝜃 ∧ 𝜏)))) ∧ (jph ↔ ((𝜂 ⊻ 𝜁) ∨ 𝜑))) ∧ (jps ↔ ((𝜎 ⊻ 𝜌) ∨ 𝜓))) ∧ (jch ↔ ((𝜇 ⊻ 𝜆) ∨ 𝜒))) → ((((𝜅 ↔ ⊥) ∧ (jph ↔ ⊥)) ∧ (jps ↔ ⊤)) ∧ (jch ↔ ⊥)))
20.40  Mathbox for Adhemar
Theorem	adh-jarrsc 44495	Replacement of a nested antecedent with an outer antecedent. Commuted simplificated form of elimination of a nested antecedent. Also holds intuitionistically. Polish prefix notation: CCCpqrCsCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒)))
20.40.1  Minimal implicational calculus Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is used to denote implication in Polish prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7 } (sometimes written KS), or with { imim1 83, ax-1 6, pm2.43 56 } (written B'KW), or with { imim2 58, pm2.04 90, ax-1 6, pm2.43 56 } (written BCKW), or with the single axiom adh-minim 44496, or with the single axiom adh-minimp 44508. This section proves first adh-minim 44496 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 44508 from { ax-1 6, ax-2 7 }, also followed by the converse, also due to Ivo Thomas. Sources for this section are * Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170; * Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477, in which the derivations of { ax-1 6, ax-2 7 } from adh-minim 44496 are shortened (compared to Meredith's derivations in the aforementioned paper); * Carew Arthur Meredith and Arthur Norman Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, volume IV, number 3, July 1963, pages 171--187; and * the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm 44496 on Dolph Edward "Ted" Ulrich's website, where these and other single axioms for the minimal implicational calculus are listed. This entire section also holds intuitionistically. Users of the Polish prefix notation also often use a compact notation for proof derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 6 from ax-2 7, that is, using modus ponens ax-mp 5 with ax-1 6 as minor premise and ax-2 7 as major premise. When the numbered lemmas surpass 10, dots are added between the numbers. D-strings are accepted by the grammar Dundotted := digit | "D" Dundotted Dundotted ; Ddotted := digit + | "D" Ddotted "." Ddotted ; Dstr := Dundotted | Ddotted . (Contributed by BJ, 11-Apr-2021.) (Revised by ADH, 10-Nov-2023.)
Theorem	adh-minim 44496	A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. This is the axiom from Carew Arthur Meredith, A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. A two-line review by Alonzo Church of this article can be found in The Journal of Symbolic Logic, volume 19, issue 2, June 1954, page 144, https://doi.org/10.2307/2268914. Known as "HI-1" on Dolph Edward "Ted" Ulrich's web page. In the next 6 lemmas and 3 theorems, ax-1 6 and ax-2 7 are derived from this single axiom in 16 detachments (instances of ax-mp 5) in total. Polish prefix notation: CCCpqrCsCCqCrtCqt . (Contributed by ADH, 10-Nov-2023.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → ((𝜓 → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
Theorem	adh-minim-ax1-ax2-lem1 44497	First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CpCCqCCrCCsCqtCstuCqu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ((𝜓 → ((𝜒 → ((𝜃 → (𝜓 → 𝜏)) → (𝜃 → 𝜏))) → 𝜂)) → (𝜓 → 𝜂)))
Theorem	adh-minim-ax1-ax2-lem2 44498	Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCpCCqCCrCpsCrstCpt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → ((𝜓 → ((𝜒 → (𝜑 → 𝜃)) → (𝜒 → 𝜃))) → 𝜏)) → (𝜑 → 𝜏))
Theorem	adh-minim-ax1-ax2-lem3 44499	Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCpCqrCqCsCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜃 → (𝜑 → 𝜒))))
Theorem	adh-minim-ax1-ax2-lem4 44500	Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 44496 and ax-mp 5. Polish prefix notation: CCCpqrCCqCrsCqs . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜃)) → (𝜓 → 𝜃)))