Home | Metamath
Proof Explorer Theorem List (p. 419 of 470) | < 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: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rp-frege4g 41801 | Deduction related to distribution. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))) | ||
Theorem | frege4 41802 | Special case of closed form of a2d 29. Special case of rp-frege4g 41801. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | ||
Theorem | frege5 41803 | 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 41804 | Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜃 → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))) | ||
Theorem | rp-4frege 41805 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → ((𝜓 → 𝜑) → 𝜒)) → (𝜑 → 𝜒)) | ||
Theorem | rp-6frege 41806 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ((𝜓 → ((𝜒 → 𝜓) → 𝜃)) → (𝜓 → 𝜃))) | ||
Theorem | rp-8frege 41807 | Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → ((𝜒 → 𝜓) → 𝜃))) → (𝜑 → (𝜓 → 𝜃))) | ||
Theorem | rp-frege25 41808 | Closed form for a1dd 50. Alternate route to Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
Theorem | frege6 41809 | 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 41810 |
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 41811 | 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 41812 | 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 41793, and ax-frege2 41794. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | frege26 41813 | Identical to idd 24. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜓)) | ||
Theorem | frege27 41814 | 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 41815 | Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 41803 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 41816 | A closed form of com23 86. Proposition 12 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃)))) | ||
Theorem | frege11 41817 | 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 41818 | Closed form for a1d 25. Deduction introducing an embedded antecedent. Identical to rp-frege24 41800 which was proved without relying on ax-frege8 41812. Proposition 24 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓))) | ||
Theorem | frege16 41819 | A closed form of com34 91. Proposition 16 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))) | ||
Theorem | frege25 41820 | Closed form for a1dd 50. Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
Theorem | frege18 41821 | 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 41822 | A closed form of com45 97. Proposition 22 of [Frege1879] p. 41. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) → (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂)))))) | ||
Theorem | frege10 41823 | Result commuting antecedents within an antecedent. Proposition 10 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜃) → ((𝜓 → (𝜑 → 𝜒)) → 𝜃)) | ||
Theorem | frege17 41824 | A closed form of com3l 89. Proposition 17 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||
Theorem | frege13 41825 | A closed form of com3r 87. Proposition 13 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃)))) | ||
Theorem | frege14 41826 | 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 41827 | A closed form of syl6 35. Proposition 19 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜒 → 𝜃) → (𝜑 → (𝜓 → 𝜃)))) | ||
Theorem | frege23 41828 | 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 41829 | A closed form of com4r 94. Proposition 15 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
Theorem | frege21 41830 | Replace antecedent in antecedent. Proposition 21 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜃) → ((𝜃 → 𝜓) → 𝜒))) | ||
Theorem | frege20 41831 | A closed form of syl8 76. Proposition 20 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜃 → 𝜏) → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
Theorem | axfrege28 41832 | Contraposition. Identical to con3 153. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Axiom | ax-frege28 41833 | 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 41834 | Closed form of con3d 152. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → ¬ 𝜓))) | ||
Theorem | frege30 41835 | Commuted, closed form of con3d 152. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (¬ 𝜒 → ¬ 𝜑))) | ||
Theorem | axfrege31 41836 | Identical to notnotr 130. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) |
⊢ (¬ ¬ 𝜑 → 𝜑) | ||
Axiom | ax-frege31 41837 | 𝜑 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 41838 | Deduce con1 146 from con3 153. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → ¬ ¬ 𝜑)) → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))) | ||
Theorem | frege33 41839 | 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 41840 | 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 41841 | Commuted, closed form of con1d 145. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (¬ 𝜒 → (𝜑 → 𝜓))) | ||
Theorem | frege36 41842 | 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 41843 | If 𝜒 is a necessary consequence of the occurrence of 𝜓 or 𝜑, then 𝜒 is a necessary consequence of 𝜑 alone. Similar to a closed form of orcs 874. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜒)) | ||
Theorem | frege38 41844 | Identical to pm2.21 123. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
Theorem | frege39 41845 | 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 41846 | Anything implies pm2.18 128. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → ((¬ 𝜓 → 𝜓) → 𝜓)) | ||
Theorem | axfrege41 41847 | Identical to notnot 142. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ¬ ¬ 𝜑) | ||
Axiom | ax-frege41 41848 | 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 41849 | Not not id 22. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ¬ ¬ (𝜑 → 𝜑) | ||
Theorem | frege43 41850 | 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 41851 | Similar to a commuted pm2.62 899. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
Theorem | frege45 41852 | Deduce pm2.6 190 from con1 146. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) → ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))) | ||
Theorem | frege46 41853 | 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 190. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | frege47 41854 | 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 41855 | 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 41967. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → ((𝜒 → 𝜃) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))) | ||
Theorem | frege49 41856 | Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → 𝜒))) | ||
Theorem | frege50 41857 | Closed form of jaoi 856. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((¬ 𝜑 → 𝜒) → 𝜓))) | ||
Theorem | frege51 41858 | Compare with jaod 858. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜒) → (𝜑 → ((¬ 𝜓 → 𝜃) → 𝜒)))) | ||
Here we leverage df-ifp 1063 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 41859 | Justification for ax-frege52a 41860. (Contributed by RP, 17-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
Axiom | ax-frege52a 41860 | 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 41861 | 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 214. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | frege53aid 41862 | Specialization of frege53a 41863. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ((𝜑 ↔ 𝜓) → 𝜓)) | ||
Theorem | frege53a 41863 | Lemma for frege55a 41871. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜃, 𝜒) → ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜃, 𝜒))) | ||
Theorem | axfrege54a 41864 | Justification for ax-frege54a 41865. Identical to biid 261. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 ↔ 𝜑) | ||
Axiom | ax-frege54a 41865 | 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 41866 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege54cor1a 41867 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | frege55aid 41868 | Lemma for frege57aid 41875. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege55lem1a 41869 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑))) | ||
Theorem | frege55lem2a 41870 | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55a 41871 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege55cor1a 41872 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege56aid 41873 | Lemma for frege57aid 41875. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓))) | ||
Theorem | frege56a 41874 | Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)))) | ||
Theorem | frege57aid 41875 | This is the all imporant formula which allows to apply Frege-style definitions and explore their consequences. A closed form of biimpri 227. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | frege57a 41876 | Analogue of frege57aid 41875. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃))) | ||
Theorem | axfrege58a 41877 | Identical to anifp 1071. Justification for ax-frege58a 41878. (Contributed by RP, 28-Mar-2020.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Axiom | ax-frege58a 41878 | If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2072. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | frege58acor 41879 | Lemma for frege59a 41880. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏))) | ||
Theorem | frege59a 41880 |
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 41816 incorrectly referenced where frege30 41835 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)))) | ||
Theorem | frege60a 41881 | Swap antecedents of ax-frege58a 41878. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege61a 41882 | Lemma for frege65a 41886. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | frege62a 41883 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2664 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 41884 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏)))) | ||
Theorem | frege64a 41885 | Lemma for frege65a 41886. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁)))) | ||
Theorem | frege65a 41886 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2664 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 41887 | Swap antecedents of frege65a 41886. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁)))) | ||
Theorem | frege67a 41888 | Lemma for frege68a 41889. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒)))) | ||
Theorem | frege68a 41889 | 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 41890 | Justification for ax-frege52c 41891. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Axiom | ax-frege52c 41891 | One side of dfsbcq 3740. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑)) | ||
Theorem | frege52b 41892 | 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 and the same proposition, this time where we substitute the content of 𝑦, is denied does not take place. In [𝑥 / 𝑧]𝜑, 𝑥 can also occur in other than the argument (𝑧) places. Hence 𝑥 may still be contained in [𝑦 / 𝑧]𝜑. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | frege53b 41893 | Lemma for frege102 (via frege92 41958). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑)) | ||
Theorem | axfrege54c 41894 | Reflexive equality of classes. Identical to eqid 2738. Justification for ax-frege54c 41895. (Contributed by RP, 24-Dec-2019.) |
⊢ 𝐴 = 𝐴 | ||
Axiom | ax-frege54c 41895 | Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2738. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ 𝐴 = 𝐴 | ||
Theorem | frege54b 41896 | Reflexive equality of sets. The content of 𝑥 is identical with the content of 𝑥. Part of Axiom 54 of [Frege1879] p. 50. Slightly specialized version of eqid 2738. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | frege54cor1b 41897 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) |
⊢ [𝑥 / 𝑦]𝑦 = 𝑥 | ||
Theorem | frege55lem1b 41898* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧)) | ||
Theorem | frege55lem2b 41899 | Lemma for frege55b 41900. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥) | ||
Theorem | frege55b 41900 |
Lemma for frege57b 41902. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2762 incorporates eqcom 2745 which is stronger than this proposition which is identical to equcomi 2021. Is it possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |