P. 470 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46901-47000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bothfbothsame 46901	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 46902	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 46903	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 46904	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1512 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 46905	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 46906	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 46907	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 46908	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 46909	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 46910	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 46911	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 46912	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 46913	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 46914	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 46915	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 46916	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 46917	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 46918	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 46919	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 46920	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 46921	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 46922	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 46923	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 46924	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 46925	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 46926	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 46927	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 46928	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 46929	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 46930	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 46931	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	nabctnabc 46932	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ). (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ ¬ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (¬ 𝜑 → (𝜓 ∧ 𝜒))
Theorem	jabtaib 46933	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	onenotinotbothi 46934	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 46935	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 46936	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ ¬ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftet 46937	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ (𝜑 ∧ 𝜒)    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	clifteta 46938	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ ¬ 𝜒) ∨ (𝜓 ∧ 𝜒)))
Theorem	cliftetb 46939	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
⊢ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))    &   ⊢ 𝜃    ⇒   ⊢ (𝜃 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒)))
Theorem	confun 46940	Given the hypotheses there exists a proof for (c implies ( d iff a ) ). (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜃 ↔ 𝜑))
Theorem	confun2 46941	Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜓 → 𝜑)    &   ⊢ (𝜓 → ¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)))    &   ⊢ ((𝜓 → 𝜑) → ((𝜓 → 𝜑) → 𝜑))    ⇒   ⊢ (𝜓 → (¬ (𝜓 → (𝜓 ∧ ¬ 𝜓)) ↔ (𝜓 → 𝜑)))
Theorem	confun3 46942	Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ (𝜑 ↔ (𝜒 → 𝜓))    &   ⊢ (𝜃 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ (𝜒 → 𝜓)    &   ⊢ (𝜒 → ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ ((𝜒 → 𝜓) → ((𝜒 → 𝜓) → 𝜓))    ⇒   ⊢ (𝜒 → (¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)) ↔ (𝜒 → 𝜓)))
Theorem	confun4 46943	An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.)
⊢ 𝜑    &   ⊢ ((𝜑 → 𝜓) → 𝜓)    &   ⊢ (𝜓 → (𝜑 → 𝜒))    &   ⊢ ((𝜒 → 𝜃) → ((𝜑 → 𝜃) ↔ 𝜓))    &   ⊢ (𝜏 ↔ (𝜒 → 𝜃))    &   ⊢ (𝜂 ↔ ¬ (𝜒 → (𝜒 ∧ ¬ 𝜒)))    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜒 → (𝜓 → 𝜏))
Theorem	confun5 46944	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 46945	Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜒
Theorem	pldofph 46946	Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    ⇒   ⊢ 𝜏
Theorem	plvcofph 46947	Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    ⇒   ⊢ 𝜂
Theorem	plvcofphax 46948	Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝜓) ↔ 𝜑) → (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))) ∧ (𝜑 ∧ ¬ (𝜑 ∧ ¬ 𝜑))))    &   ⊢ (𝜏 ↔ ((𝜒 → 𝜃) ∧ (𝜑 ↔ 𝜒) ∧ ((𝜑 → 𝜓) → (𝜓 ↔ 𝜃))))    &   ⊢ (𝜂 ↔ (𝜒 ∧ 𝜏))    &   ⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜃    &   ⊢ (𝜁 ↔ ¬ (𝜓 ∧ ¬ 𝜏))    ⇒   ⊢ 𝜁
Theorem	plvofpos 46949	rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.)
⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓))    &   ⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓))    &   ⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))    &   ⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂))))    &   ⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂))))    &   ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎))    &   ⊢ 𝜁    &   ⊢ 𝜎    ⇒   ⊢ 𝜌
Theorem	mdandyv0 46950	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 46951	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 46952	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 46953	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 46954	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 46955	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 46956	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 46957	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 46958	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 46959	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 46960	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 46961	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 46962	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 46963	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 46964	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 46965	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 46966	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 46967	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 46968	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 46969	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 46970	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 46971	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 46972	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 46973	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 46974	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 46975	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 46976	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 46977	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 46978	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 46979	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 46980	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 46981	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 46982	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 46983	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 46984	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 46985	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 46986	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 46987	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 46988	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 46989	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 46990	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 46991	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 46992	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 46993	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 46994	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 46995	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 46996	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 46997	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 46998	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 46999	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 47000	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 ↔ ⊥)))