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	mdandyv3 47301	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 47302	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 47303	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 47304	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 47305	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 47306	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 47307	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 47308	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 47309	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 47310	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 47311	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 47312	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 47313	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 47314	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 47315	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 47316	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 47317	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 47318	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 47319	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 47320	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 47321	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 47322	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 47323	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 47324	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 47325	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 47326	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 47327	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 47328	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 47329	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 47330	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 47331	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 47332	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 47333	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 47334	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 47335	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 47336	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 47337	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 47338	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 47339	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 47340	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 47341	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 47342	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 47343	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 47344	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 47345	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 47346	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 47347	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 47348	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 ↔ ⊥)))
21.47  Mathbox for Adhemar
Theorem	adh-jarrsc 47349	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.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒)))
21.47.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 47350, or with the single axiom adh-minimp 47362. This section proves first adh-minim 47350 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 47362 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 47350 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 47350 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 47350	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 47351	First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 47350 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 47352	Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 47350 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 47353	Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 47350 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 47354	Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 47350 and ax-mp 5. Polish prefix notation: CCCpqrCCqCrsCqs . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜓 → (𝜒 → 𝜃)) → (𝜓 → 𝜃)))
Theorem	adh-minim-ax1 47355	Derivation of ax-1 6 from adh-minim 47350 and ax-mp 5. Carew Arthur Meredith derived ax-1 6 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CpCqp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	adh-minim-ax2-lem5 47356	Fifth lemma for the derivation of ax-2 7 from adh-minim 47350 and ax-mp 5. Polish prefix notation: CpCCCqrsCCrCstCrt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (((𝜓 → 𝜒) → 𝜃) → ((𝜒 → (𝜃 → 𝜏)) → (𝜒 → 𝜏))))
Theorem	adh-minim-ax2-lem6 47357	Sixth lemma for the derivation of ax-2 7 from adh-minim 47350 and ax-mp 5. Polish prefix notation: CCpCCCCqrsCCrCstCrtuCpu . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → ((((𝜓 → 𝜒) → 𝜃) → ((𝜒 → (𝜃 → 𝜏)) → (𝜒 → 𝜏))) → 𝜂)) → (𝜑 → 𝜂))
Theorem	adh-minim-ax2c 47358	Derivation of a commuted form of ax-2 7 from adh-minim 47350 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
Theorem	adh-minim-ax2 47359	Derivation of ax-2 7 from adh-minim 47350 and ax-mp 5. Carew Arthur Meredith derived ax-2 7 in A single axiom of positive logic, The Journal of Computing Systems, volume 1, issue 3, July 1953, pages 169--170. However, here we follow the shortened derivation by Ivo Thomas, On Meredith's sole positive axiom, Notre Dame Journal of Formal Logic, volume XV, number 3, July 1974, page 477. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	adh-minim-idALT 47360	Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 47355, adh-minim-ax2 47359, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜑)
Theorem	adh-minim-pm2.43 47361	Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 47355, adh-minim-ax2 47359, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	adh-minimp 47362	Another 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. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). Known as "HI-2" on Dolph Edward "Ted" Ulrich's web page. In the next 4 lemmas and 5 theorems, ax-1 6 and ax-2 7 are derived from this other single axiom in 20 detachments (instances of ax-mp 5) in total. Polish prefix notation: CpCCqrCCCsqCrtCqt ; or CtCCpqCCCspCqrCpr in 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, on page 180. (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.)
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
Theorem	adh-minimp-jarr-imim1-ax2c-lem1 47363	First lemma for the derivation of jarr 106, imim1 83, and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7, from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCpqCCCrpCqsCps . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃)))
Theorem	adh-minimp-jarr-lem2 47364	Second lemma for the derivation of jarr 106, and indirectly ax-1 6, a commuted form of ax-2 7, and ax-2 7 proper, from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCCpqCCCrsCCCtrCsuCruvCqv . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → (((𝜒 → 𝜃) → (((𝜏 → 𝜒) → (𝜃 → 𝜂)) → (𝜒 → 𝜂))) → 𝜁)) → (𝜓 → 𝜁))
Theorem	adh-minimp-jarr-ax2c-lem3 47365	Third lemma for the derivation of jarr 106 and a commuted form of ax-2 7, and indirectly ax-1 6 and ax-2 7 proper , from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCCCpqCCCrpCqsCpstt . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → (((𝜒 → 𝜑) → (𝜓 → 𝜃)) → (𝜑 → 𝜃))) → 𝜏) → 𝜏)
Theorem	adh-minimp-sylsimp 47366	Derivation of jarr 106 (also called "syll-simp") from minimp 1623 and ax-mp 5. Polish prefix notation: CCCpqrCqr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	adh-minimp-ax1 47367	Derivation of ax-1 6 from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CpCqp . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	adh-minimp-imim1 47368	Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCpqCCqrCpr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	adh-minimp-ax2c 47369	Derivation of a commuted form of ax-2 7 from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCpqCCpCqrCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
Theorem	adh-minimp-ax2-lem4 47370	Fourth lemma for the derivation of ax-2 7 from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CpCCqCprCqr . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ((𝜓 → (𝜑 → 𝜒)) → (𝜓 → 𝜒)))
Theorem	adh-minimp-ax2 47371	Derivation of ax-2 7 from adh-minimp 47362 and ax-mp 5. Polish prefix notation: CCpCqrCCpqCpr . (Contributed by BJ, 4-Apr-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	adh-minimp-idALT 47372	Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 47367, adh-minimp-ax2 47371, and ax-mp 5. It uses the derivation written DD211 in D-notation. (See head comment for an explanation.) Polish prefix notation: Cpp . (Contributed by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜑)
Theorem	adh-minimp-pm2.43 47373	Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 47367, adh-minimp-ax2 47371, and ax-mp 5. It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021.) (Revised by ADH, 10-Nov-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
21.48  Mathbox for Alexander van der Vekens
21.48.1  General auxiliary theorems (1)
21.48.1.1  Unordered and ordered pairs - extension for singletons
Theorem	n0nsn2el 47374*	If a class with one element is not a singleton, there is at least another element in this class. (Contributed by AV, 6-Mar-2025.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ≠ {𝐴}) → ∃𝑥 ∈ 𝐵 𝑥 ≠ 𝐴)
Theorem	eusnsn 47375*	There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.)
⊢ ∃!𝑥{𝑥} = {𝑦}
Theorem	absnsb 47376*	If the class abstraction {𝑥 ∣ 𝜑} associated with the wff 𝜑 is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022.)
⊢ ({𝑥 ∣ 𝜑} = {𝑦} → [𝑦 / 𝑥]𝜑)
Theorem	euabsneu 47377*	Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4684 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.)
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦})
21.48.1.2  Unordered and ordered pairs - extension for unordered pairs
Theorem	elprneb 47378	An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.)
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶))
21.48.1.3  Unordered and ordered pairs - extension for ordered pairs
Theorem	oppr 47379	Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴, 𝐵} = {𝐶, 𝐷}))
Theorem	opprb 47380	Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ∨ ⟨𝐴, 𝐵⟩ = ⟨𝐷, 𝐶⟩)))
Theorem	or2expropbilem1 47381*	Lemma 1 for or2expropbi 47383 and ich2exprop 47820. (Contributed by AV, 16-Jul-2023.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))))
Theorem	or2expropbilem2 47382*	Lemma 2 for or2expropbi 47383 and ich2exprop 47820. (Contributed by AV, 16-Jul-2023.)
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑))
Theorem	or2expropbi 47383*	If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
21.48.1.4  Relations - extension
Theorem	eubrv 47384*	If there is a unique set which is related to a class, then the class must be a set. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ V)
Theorem	eubrdm 47385*	If there is a unique set which is related to a class, then the class is an element of the domain of the relation. (Contributed by AV, 25-Aug-2022.)
⊢ (∃!𝑏 𝐴𝑅𝑏 → 𝐴 ∈ dom 𝑅)
Theorem	eldmressn 47386	Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴)
21.48.1.5  Definite description binder (inverted iota) - extension
Theorem	iota0def 47387*	Example for a defined iota being the empty set, i.e., ∀𝑦𝑥 ⊆ 𝑦 is a wff satisfied by a unique value 𝑥, namely 𝑥 = ∅ (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022.)
⊢ (℩𝑥∀𝑦 𝑥 ⊆ 𝑦) = ∅
Theorem	iota0ndef 47388*	Example for an undefined iota being the empty set, i.e., ∀𝑦𝑦 ∈ 𝑥 is a wff not satisfied by a (unique) value 𝑥 (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022.)
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅
21.48.1.6  Functions - extension
Theorem	fveqvfvv 47389	If a function's value at an argument is the universal class (which can never be the case because of fvex 6855), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 119). (Contributed by Alexander van der Vekens, 26-May-2017.)
⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵)
Theorem	fnresfnco 47390	Composition of two functions, similar to fnco 6618. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵)
Theorem	funcoressn 47391	A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}))
Theorem	funressnfv 47392	A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))
Theorem	funressndmfvrn 47393	The value of a function 𝐹 at a set 𝐴 is in the range of the function 𝐹 if 𝐴 is in the domain of the function 𝐹. It is sufficient that 𝐹 is a function at 𝐴. (Contributed by AV, 1-Sep-2022.)
⊢ ((Fun (𝐹 ↾ {𝐴}) ∧ 𝐴 ∈ dom 𝐹) → (𝐹‘𝐴) ∈ ran 𝐹)
Theorem	funressnvmo 47394*	A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.)
⊢ (Fun (𝐹 ↾ {𝑥}) → ∃*𝑦 𝑥𝐹𝑦)
Theorem	funressnmo 47395*	A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ Fun (𝐹 ↾ {𝐴})) → ∃*𝑦 𝐴𝐹𝑦)
Theorem	funressneu 47396*	There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6525. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6832. (Contributed by AV, 7-Sep-2022.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦)
Theorem	fresfo 47397	Conditions for a restriction to be an onto function. Part of fresf1o 32720. (Contributed by AV, 29-Sep-2024.)
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶)
Theorem	fsetsniunop 47398*	The class of all functions from a (proper) singleton into 𝐵 is the union of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.)
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = ∪ 𝑏 ∈ 𝐵 {{⟨𝑆, 𝑏⟩}})
Theorem	fsetabsnop 47399*	The class of all functions from a (proper) singleton into 𝐵 is the class of all the singletons of (proper) ordered pairs over the elements of 𝐵 as second component. (Contributed by AV, 13-Sep-2024.)
⊢ (𝑆 ∈ 𝑉 → {𝑓 ∣ 𝑓:{𝑆}⟶𝐵} = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}})
Theorem	fsetsnf 47400*	The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.)
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {⟨𝑆, 𝑏⟩}}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {⟨𝑆, 𝑥⟩})    ⇒   ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴)