| Metamath
Proof Explorer Theorem List (p. 439 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | psshepw 43801 | The relation between sets and their proper subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.) |
| ⊢ ◡ [⊊] hereditary 𝒫 𝐴 | ||
| Theorem | sshepw 43802 | The relation between sets and their subsets is hereditary in the powerclass of any class. (Contributed by RP, 28-Mar-2020.) |
| ⊢ (◡ [⊊] ∪ I ) hereditary 𝒫 𝐴 | ||
| Axiom | ax-frege1 43803 | The case in which 𝜑 is denied, 𝜓 is affirmed, and 𝜑 is affirmed is excluded. This is evident since 𝜑 cannot at the same time be denied and affirmed. Axiom 1 of [Frege1879] p. 26. Identical to ax-1 6. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜑)) | ||
| Axiom | ax-frege2 43804 | If a proposition 𝜒 is a necessary consequence of two propositions 𝜓 and 𝜑 and one of those, 𝜓, is in turn a necessary consequence of the other, 𝜑, then the proposition 𝜒 is a necessary consequence of the latter one, 𝜑, alone. Axiom 2 of [Frege1879] p. 26. Identical to ax-2 7. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
| Theorem | rp-simp2-frege 43805 | Simplification of triple conjunction. Compare with simp2 1138. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓))) | ||
| Theorem | rp-simp2 43806 | Simplification of triple conjunction. Identical to simp2 1138. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
| Theorem | rp-frege3g 43807 |
Add antecedent to ax-frege2 43804. More general statement than frege3 43808.
Like ax-frege2 43804, it is essentially a closed form of mpd 15,
however it
has an extra antecedent.
It would be more natural to prove from a1i 11 and ax-frege2 43804 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))) | ||
| Theorem | frege3 43808 | Add antecedent to ax-frege2 43804. Special case of rp-frege3g 43807. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜑 → 𝜓)) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | ||
| Theorem | rp-misc1-frege 43809 | Double-use of ax-frege2 43804. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜓)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
| Theorem | rp-frege24 43810 | Introducing an embedded antecedent. Alternate proof for frege24 43828. Closed form for a1d 25. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓))) | ||
| Theorem | rp-frege4g 43811 | Deduction related to distribution. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))) | ||
| Theorem | frege4 43812 | Special case of closed form of a2d 29. Special case of rp-frege4g 43811. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | ||
| Theorem | frege5 43813 | A closed form of syl 17. Identical to imim2 58. Theorem *2.05 of [WhiteheadRussell] p. 100. Proposition 5 of [Frege1879] p. 32. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))) | ||
| Theorem | rp-7frege 43814 | Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜃 → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))) | ||
| Theorem | rp-4frege 43815 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → ((𝜓 → 𝜑) → 𝜒)) → (𝜑 → 𝜒)) | ||
| Theorem | rp-6frege 43816 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → ((𝜓 → ((𝜒 → 𝜓) → 𝜃)) → (𝜓 → 𝜃))) | ||
| Theorem | rp-8frege 43817 | Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → (𝜓 → ((𝜒 → 𝜓) → 𝜃))) → (𝜑 → (𝜓 → 𝜃))) | ||
| Theorem | rp-frege25 43818 | Closed form for a1dd 50. Alternate route to Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
| Theorem | frege6 43819 | A closed form of imim2d 57 which is a deduction adding nested antecedents. Proposition 6 of [Frege1879] p. 33. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → ((𝜃 → 𝜓) → (𝜃 → 𝜒)))) | ||
| Theorem | axfrege8 43820 |
Swap antecedents. Identical to pm2.04 90. This demonstrates that Axiom 8
of [Frege1879] p. 35 is redundant.
Proof follows closely proof of pm2.04 90 in https://us.metamath.org/mmsolitaire/pmproofs.txt 90, but in the style of Frege's 1879 work. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
| Theorem | frege7 43821 | A closed form of syl6 35. The first antecedent is used to replace the consequent of the second antecedent. Proposition 7 of [Frege1879] p. 34. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜃 → 𝜑)) → (𝜒 → (𝜃 → 𝜓)))) | ||
| Axiom | ax-frege8 43822 | Swap antecedents. If two conditions have a proposition as a consequence, their order is immaterial. Third axiom of Frege's 1879 work but identical to pm2.04 90 which can be proved from only ax-mp 5, ax-frege1 43803, and ax-frege2 43804. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
| Theorem | frege26 43823 | Identical to idd 24. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → (𝜓 → 𝜓)) | ||
| Theorem | frege27 43824 | We cannot (at the same time) affirm 𝜑 and deny 𝜑. Identical to id 22. Proposition 27 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → 𝜑) | ||
| Theorem | frege9 43825 | Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 43813 only in an unessential way. Identical to imim1 83. Proposition 9 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
| Theorem | frege12 43826 | A closed form of com23 86. Proposition 12 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃)))) | ||
| Theorem | frege11 43827 | Elimination of a nested antecedent as a partial converse of ja 186. If the proposition that 𝜓 takes place or 𝜑 does not is a sufficient condition for 𝜒, then 𝜓 by itself is a sufficient condition for 𝜒. Identical to jarr 106. Proposition 11 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
| Theorem | frege24 43828 | Closed form for a1d 25. Deduction introducing an embedded antecedent. Identical to rp-frege24 43810 which was proved without relying on ax-frege8 43822. Proposition 24 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓))) | ||
| Theorem | frege16 43829 | A closed form of com34 91. Proposition 16 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))) | ||
| Theorem | frege25 43830 | Closed form for a1dd 50. Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
| Theorem | frege18 43831 | Closed form of a syllogism followed by a swap of antecedents. Proposition 18 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜑) → (𝜓 → (𝜃 → 𝜒)))) | ||
| Theorem | frege22 43832 | A closed form of com45 97. Proposition 22 of [Frege1879] p. 41. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) → (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂)))))) | ||
| Theorem | frege10 43833 | Result commuting antecedents within an antecedent. Proposition 10 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜃) → ((𝜓 → (𝜑 → 𝜒)) → 𝜃)) | ||
| Theorem | frege17 43834 | A closed form of com3l 89. Proposition 17 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||
| Theorem | frege13 43835 | A closed form of com3r 87. Proposition 13 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃)))) | ||
| Theorem | frege14 43836 | Closed form of a deduction based on com3r 87. Proposition 14 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜃 → (𝜓 → (𝜒 → 𝜏))))) | ||
| Theorem | frege19 43837 | A closed form of syl6 35. Proposition 19 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜒 → 𝜃) → (𝜑 → (𝜓 → 𝜃)))) | ||
| Theorem | frege23 43838 | Syllogism followed by rotation of three antecedents. Proposition 23 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜏 → 𝜑) → (𝜓 → (𝜒 → (𝜏 → 𝜃))))) | ||
| Theorem | frege15 43839 | A closed form of com4r 94. Proposition 15 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
| Theorem | frege21 43840 | Replace antecedent in antecedent. Proposition 21 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜃) → ((𝜃 → 𝜓) → 𝜒))) | ||
| Theorem | frege20 43841 | A closed form of syl8 76. Proposition 20 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜃 → 𝜏) → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
| Theorem | axfrege28 43842 | Contraposition. Identical to con3 153. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
| Axiom | ax-frege28 43843 | Contraposition. Identical to con3 153. Theorem *2.16 of [WhiteheadRussell] p. 103. Axiom 28 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
| Theorem | frege29 43844 | Closed form of con3d 152. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → ¬ 𝜓))) | ||
| Theorem | frege30 43845 | Commuted, closed form of con3d 152. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (¬ 𝜒 → ¬ 𝜑))) | ||
| Theorem | axfrege31 43846 | Identical to notnotr 130. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (¬ ¬ 𝜑 → 𝜑) | ||
| Axiom | ax-frege31 43847 | 𝜑 cannot be denied and (at the same time ) ¬ ¬ 𝜑 affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnotr 130. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ (¬ ¬ 𝜑 → 𝜑) | ||
| Theorem | frege32 43848 | Deduce con1 146 from con3 153. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → ¬ ¬ 𝜑)) → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))) | ||
| Theorem | frege33 43849 | If 𝜑 or 𝜓 takes place, then 𝜓 or 𝜑 takes place. Identical to con1 146. Proposition 33 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) | ||
| Theorem | frege34 43850 | If as a consequence of the occurrence of the circumstance 𝜑, when the obstacle 𝜓 is removed, 𝜒 takes place, then from the circumstance that 𝜒 does not take place while 𝜑 occurs the occurrence of the obstacle 𝜓 can be inferred. Closed form of con1d 145. Proposition 34 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → 𝜓))) | ||
| Theorem | frege35 43851 | Commuted, closed form of con1d 145. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (¬ 𝜒 → (𝜑 → 𝜓))) | ||
| Theorem | frege36 43852 | The case in which 𝜓 is denied, ¬ 𝜑 is affirmed, and 𝜑 is affirmed does not occur. If 𝜑 occurs, then (at least) one of the two, 𝜑 or 𝜓, takes place (no matter what 𝜓 might be). Identical to pm2.24 124. Proposition 36 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
| Theorem | frege37 43853 | If 𝜒 is a necessary consequence of the occurrence of 𝜓 or 𝜑, then 𝜒 is a necessary consequence of 𝜑 alone. Similar to a closed form of orcs 876. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜒)) | ||
| Theorem | frege38 43854 | Identical to pm2.21 123. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
| Theorem | frege39 43855 | Syllogism between pm2.18 128 and pm2.24 124. Proposition 39 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜑) → (¬ 𝜑 → 𝜓)) | ||
| Theorem | frege40 43856 | Anything implies pm2.18 128. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (¬ 𝜑 → ((¬ 𝜓 → 𝜓) → 𝜓)) | ||
| Theorem | axfrege41 43857 | Identical to notnot 142. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 → ¬ ¬ 𝜑) | ||
| Axiom | ax-frege41 43858 | The affirmation of 𝜑 denies the denial of 𝜑. Identical to notnot 142. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ (𝜑 → ¬ ¬ 𝜑) | ||
| Theorem | frege42 43859 | Not not id 22. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ¬ ¬ (𝜑 → 𝜑) | ||
| Theorem | frege43 43860 | If there is a choice only between 𝜑 and 𝜑, then 𝜑 takes place. Identical to pm2.18 128. Proposition 43 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
| Theorem | frege44 43861 | Similar to a commuted pm2.62 900. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
| Theorem | frege45 43862 | Deduce pm2.6 191 from con1 146. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) → ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))) | ||
| Theorem | frege46 43863 | If 𝜓 holds when 𝜑 occurs as well as when 𝜑 does not occur, then 𝜓 holds. If 𝜓 or 𝜑 occurs and if the occurrences of 𝜑 has 𝜓 as a necessary consequence, then 𝜓 takes place. Identical to pm2.6 191. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
| Theorem | frege47 43864 | Deduce consequence follows from either path implied by a disjunction. If 𝜑, as well as 𝜓 is sufficient condition for 𝜒 and 𝜓 or 𝜑 takes place, then the proposition 𝜒 holds. Proposition 47 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜒) → ((𝜑 → 𝜒) → 𝜒))) | ||
| Theorem | frege48 43865 | Closed form of syllogism with internal disjunction. If 𝜑 is a sufficient condition for the occurrence of 𝜒 or 𝜓 and if 𝜒, as well as 𝜓, is a sufficient condition for 𝜃, then 𝜑 is a sufficient condition for 𝜃. See application in frege101 43977. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → ((𝜒 → 𝜃) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))) | ||
| Theorem | frege49 43866 | Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → 𝜒))) | ||
| Theorem | frege50 43867 | Closed form of jaoi 858. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((¬ 𝜑 → 𝜒) → 𝜓))) | ||
| Theorem | frege51 43868 | Compare with jaod 860. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜒) → (𝜑 → ((¬ 𝜓 → 𝜃) → 𝜒)))) | ||
Here we leverage df-ifp 1064 to partition a wff into two that are disjoint with the selector wff. Thus if we are given ⊢ (𝜑 ↔ if-(𝜓, 𝜒, 𝜃)) then we replace the concept (illegal in our notation ) (𝜑‘𝜓) with if-(𝜓, 𝜒, 𝜃) to reason about the values of the "function." Likewise, we replace the similarly illegal concept ∀𝜓𝜑 with (𝜒 ∧ 𝜃). | ||
| Theorem | axfrege52a 43869 | Justification for ax-frege52a 43870. (Contributed by RP, 17-Apr-2020.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
| Axiom | ax-frege52a 43870 | The case when the content of 𝜑 is identical with the content of 𝜓 and in which a proposition controlled by an element for which we substitute the content of 𝜑 is affirmed (in this specific case the identity logical function) and the same proposition, this time where we substituted the content of 𝜓, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
| Theorem | frege52aid 43871 | The case when the content of 𝜑 is identical with the content of 𝜓 and in which 𝜑 is affirmed and 𝜓 is denied does not take place. Identical to biimp 215. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | ||
| Theorem | frege53aid 43872 | Specialization of frege53a 43873. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (𝜑 → ((𝜑 ↔ 𝜓) → 𝜓)) | ||
| Theorem | frege53a 43873 | Lemma for frege55a 43881. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (if-(𝜑, 𝜃, 𝜒) → ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜃, 𝜒))) | ||
| Theorem | axfrege54a 43874 | Justification for ax-frege54a 43875. Identical to biid 261. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝜑 ↔ 𝜑) | ||
| Axiom | ax-frege54a 43875 | Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 261. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| ⊢ (𝜑 ↔ 𝜑) | ||
| Theorem | frege54cor0a 43876 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
| Theorem | frege54cor1a 43877 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
| Theorem | frege55aid 43878 | Lemma for frege57aid 43885. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
| ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
| Theorem | frege55lem1a 43879 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑))) | ||
| Theorem | frege55lem2a 43880 | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
| Theorem | frege55a 43881 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
| Theorem | frege55cor1a 43882 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
| Theorem | frege56aid 43883 | Lemma for frege57aid 43885. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓))) | ||
| Theorem | frege56a 43884 | Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)))) | ||
| Theorem | frege57aid 43885 | This is the all important formula which allows to apply Frege-style definitions and explore their consequences. A closed form of biimpri 228. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
| Theorem | frege57a 43886 | Analogue of frege57aid 43885. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) | ||
| Theorem | axfrege58a 43887 | Identical to anifp 1072. Justification for ax-frege58a 43888. (Contributed by RP, 28-Mar-2020.) |
| ⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
| Axiom | ax-frege58a 43888 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2068. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
| ⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
| Theorem | frege58acor 43889 | Lemma for frege59a 43890. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
| Theorem | frege59a 43890 |
A kind of Aristotelian inference. Namely Felapton or Fesapo. Proposition
59 of [Frege1879] p. 51.
Note: in the Bauer-Meenfelberg translation published in van Heijenoort's collection From Frege to Goedel, this proof has the frege12 43826 incorrectly referenced where frege30 43845 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)))) | ||
| Theorem | frege60a 43891 | Swap antecedents of ax-frege58a 43888. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
| Theorem | frege61a 43892 | Lemma for frege65a 43896. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
| Theorem | frege62a 43893 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (if-(𝜑, 𝜓, 𝜃) → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏))) | ||
| Theorem | frege63a 43894 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏)))) | ||
| Theorem | frege64a 43895 | Lemma for frege65a 43896. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁)))) | ||
| Theorem | frege65a 43896 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2663 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
| Theorem | frege66a 43897 | Swap antecedents of frege65a 43896. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
| Theorem | frege67a 43898 | Lemma for frege68a 43899. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒)))) | ||
| Theorem | frege68a 43899 | Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| ⊢ (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒))) | ||
| Theorem | axfrege52c 43900 | Justification for ax-frege52c 43901. (Contributed by RP, 24-Dec-2019.) |
| ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |