![]() |
Metamath
Proof Explorer Theorem List (p. 470 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mdandyv3 46901 | 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 46902 | 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 46903 | 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 46904 | 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 46905 | 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 46906 | 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 46907 | 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 46908 | 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 46909 | 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 46910 | 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 46911 | 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 46912 | 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 46913 | 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 46914 | 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 46915 | 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 46916 | 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 46917 | 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 46918 | 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 46919 | 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 46920 | 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 46921 | 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 46922 | 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 46923 | 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 46924 | 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 46925 | 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 46926 | 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 46927 | 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 46928 | 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 46929 | 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 46930 | 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 46931 | 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 46932 | 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 46933 | 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 46934 | 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 46935 | 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 46936 | 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 46937 | 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 46938 | 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 46939 | 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 46940 | 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 46941 | 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 46942 | 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 46943 | 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 46944 | 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 46945 | 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 46946 | 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 46947 |
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 46948 |
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 ↔ ⊥))) | ||
Theorem | adh-jarrsc 46949 | 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.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜃 → (𝜓 → 𝜒))) | ||
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 46950, or with the single axiom adh-minimp 46962. This section proves first adh-minim 46950 from { ax-1 6, ax-2 7 }, followed by the converse, due to Ivo Thomas; and then it proves adh-minimp 46962 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 46950 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 46950 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 46950 | 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 46951 | First lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46950 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 46952 | Second lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46950 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 46953 | Third lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46950 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 46954 | Fourth lemma for the derivation of ax-1 6 and ax-2 7 from adh-minim 46950 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 46955 | Derivation of ax-1 6 from adh-minim 46950 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 46956 | Fifth lemma for the derivation of ax-2 7 from adh-minim 46950 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 46957 | Sixth lemma for the derivation of ax-2 7 from adh-minim 46950 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 46958 | Derivation of a commuted form of ax-2 7 from adh-minim 46950 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 46959 | Derivation of ax-2 7 from adh-minim 46950 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 46960 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minim-ax1 46955, adh-minim-ax2 46959, 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 46961 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minim-ax1 46955, adh-minim-ax2 46959, 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 46962 | 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 46963 | 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 46962 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 46964 | 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 46962 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 46965 | 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 46962 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 46966 | Derivation of jarr 106 (also called "syll-simp") from minimp 1617 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 46967 | Derivation of ax-1 6 from adh-minimp 46962 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 46968 | Derivation of imim1 83 ("left antimonotonicity of implication", theorem *2.06 of [WhiteheadRussell] p. 100) from adh-minimp 46962 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 46969 | Derivation of a commuted form of ax-2 7 from adh-minimp 46962 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 46970 | Fourth lemma for the derivation of ax-2 7 from adh-minimp 46962 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 46971 | Derivation of ax-2 7 from adh-minimp 46962 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 46972 | Derivation of id 22 (reflexivity of implication, PM *2.08 WhiteheadRussell p. 101) from adh-minimp-ax1 46967, adh-minimp-ax2 46971, 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 46973 | Derivation of pm2.43 56 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 46967, adh-minimp-ax2 46971, 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.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | n0nsn2el 46974* | 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 46975* | There is a unique element of a singleton which is equal to another singleton. (Contributed by AV, 24-Aug-2022.) |
⊢ ∃!𝑥{𝑥} = {𝑦} | ||
Theorem | absnsb 46976* | 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 46977* | Another way to express existential uniqueness of a wff 𝜑: its associated class abstraction {𝑥 ∣ 𝜑} is a singleton. Variant of euabsn2 4729 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022.) |
⊢ (∃!𝑥𝜑 ↔ ∃!𝑦{𝑥 ∣ 𝜑} = {𝑦}) | ||
Theorem | elprneb 46978 | An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.) |
⊢ ((𝐴 ∈ {𝐵, 𝐶} ∧ 𝐵 ≠ 𝐶) → (𝐴 = 𝐵 ↔ 𝐴 ≠ 𝐶)) | ||
Theorem | oppr 46979 | Equality for ordered pairs implies equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 → {𝐴, 𝐵} = {𝐶, 𝐷})) | ||
Theorem | opprb 46980 | Equality for unordered pairs corresponds to equality of unordered pairs with the same elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ∨ 〈𝐴, 𝐵〉 = 〈𝐷, 𝐶〉))) | ||
Theorem | or2expropbilem1 46981* | Lemma 1 for or2expropbi 46983 and ich2exprop 47395. (Contributed by AV, 16-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → (𝜑 → ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)))) | ||
Theorem | or2expropbilem2 46982* | Lemma 2 for or2expropbi 46983 and ich2exprop 47395. (Contributed by AV, 16-Jul-2023.) |
⊢ (∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ 𝜑) ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜑)) | ||
Theorem | or2expropbi 46983* | 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 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(〈𝐴, 𝐵〉 = 〈𝑎, 𝑏〉 ∧ (𝑎𝑅𝑏 ∧ 𝜑)))) | ||
Theorem | eubrv 46984* | 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 46985* | 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 46986 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
⊢ (𝐵 ∈ dom (𝐹 ↾ {𝐴}) → 𝐵 = 𝐴) | ||
Theorem | iota0def 46987* | 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 46988* | 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.) |
⊢ (℩𝑥∀𝑦 𝑦 ∈ 𝑥) = ∅ | ||
Theorem | fveqvfvv 46989 | If a function's value at an argument is the universal class (which can never be the case because of fvex 6919), 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 46990 | Composition of two functions, similar to fnco 6686. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
⊢ (((𝐹 ↾ ran 𝐺) Fn ran 𝐺 ∧ 𝐺 Fn 𝐵) → (𝐹 ∘ 𝐺) Fn 𝐵) | ||
Theorem | funcoressn 46991 | 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 46992 | 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 46993 | 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 46994* | 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 46995* | 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 46996* | There is exactly one value of a class which is a function restricted to a singleton, analogous to funeu 6592. 𝐴 ∈ V is required because otherwise ∃!𝑦𝐴𝐹𝑦, see brprcneu 6896. (Contributed by AV, 7-Sep-2022.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}) ∧ 𝐴𝐹𝐵) → ∃!𝑦 𝐴𝐹𝑦) | ||
Theorem | fresfo 46997 | Conditions for a restriction to be an onto function. Part of fresf1o 32647. (Contributed by AV, 29-Sep-2024.) |
⊢ ((Fun 𝐹 ∧ 𝐶 ⊆ ran 𝐹) → (𝐹 ↾ (◡𝐹 “ 𝐶)):(◡𝐹 “ 𝐶)–onto→𝐶) | ||
Theorem | fsetsniunop 46998* | 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 46999* | 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 47000* | The mapping of an element of a class to a singleton function is a function. (Contributed by AV, 13-Sep-2024.) |
⊢ 𝐴 = {𝑦 ∣ ∃𝑏 ∈ 𝐵 𝑦 = {〈𝑆, 𝑏〉}} & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ {〈𝑆, 𝑥〉}) ⇒ ⊢ (𝑆 ∈ 𝑉 → 𝐹:𝐵⟶𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |