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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfxor5 41801 | Express exclusive-or in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 14-Apr-2020.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ ((𝜑 → ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓))) | ||
Theorem | df3or2 41802 | Express triple-or in terms of implication and negation. Statement in [Frege1879] p. 11. (Contributed by RP, 25-Jul-2020.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 → (¬ 𝜓 → 𝜒))) | ||
Theorem | df3an2 41803 | Express triple-and in terms of implication and negation. Statement in [Frege1879] p. 12. (Contributed by RP, 25-Jul-2020.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (𝜑 → (𝜓 → ¬ 𝜒))) | ||
Theorem | nev 41804* | Express that not every set is in a class. (Contributed by RP, 16-Apr-2020.) |
⊢ (𝐴 ≠ V ↔ ¬ ∀𝑥 𝑥 ∈ 𝐴) | ||
Theorem | 0pssin 41805* | Express that an intersection is not empty. (Contributed by RP, 16-Apr-2020.) |
⊢ (∅ ⊊ (𝐴 ∩ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | ||
The statement 𝑅 hereditary 𝐴 means relation 𝑅 is hereditary (in the sense of Frege) in the class 𝐴 or (𝑅 “ 𝐴) ⊆ 𝐴. The former is only a slight reduction in the number of symbols, but this reduces the number of floating hypotheses needed to be checked. As Frege was not using the language of classes or sets, this naturally differs from the set-theoretic notion that a set is hereditary in a property: that all of its elements have a property and all of their elements have the property and so-on. | ||
Syntax | whe 41806 | The property of relation 𝑅 being hereditary in class 𝐴. |
wff 𝑅 hereditary 𝐴 | ||
Definition | df-he 41807 | The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 “ 𝐴) ⊆ 𝐴) | ||
Theorem | dfhe2 41808 | The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐴)) | ||
Theorem | dfhe3 41809* | The property of relation 𝑅 being hereditary in class 𝐴. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 hereditary 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦(𝑥𝑅𝑦 → 𝑦 ∈ 𝐴))) | ||
Theorem | heeq12 41810 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵) → (𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐵)) | ||
Theorem | heeq1 41811 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑅 = 𝑆 → (𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐴)) | ||
Theorem | heeq2 41812 | Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝐴 = 𝐵 → (𝑅 hereditary 𝐴 ↔ 𝑅 hereditary 𝐵)) | ||
Theorem | sbcheg 41813 | Distribute proper substitution through herditary relation. (Contributed by RP, 29-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝐵 hereditary 𝐶 ↔ ⦋𝐴 / 𝑥⦌𝐵 hereditary ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | hess 41814 | Subclass law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020.) |
⊢ (𝑆 ⊆ 𝑅 → (𝑅 hereditary 𝐴 → 𝑆 hereditary 𝐴)) | ||
Theorem | xphe 41815 | Any Cartesian product is hereditary in its second class. (Contributed by RP, 27-Mar-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (𝐴 × 𝐵) hereditary 𝐵 | ||
Theorem | 0he 41816 | The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) |
⊢ ∅ hereditary 𝐴 | ||
Theorem | 0heALT 41817 | The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∅ hereditary 𝐴 | ||
Theorem | he0 41818 | Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020.) |
⊢ 𝐴 hereditary ∅ | ||
Theorem | unhe1 41819 | The union of two relations hereditary in a class is also hereditary in a class. (Contributed by RP, 28-Mar-2020.) |
⊢ ((𝑅 hereditary 𝐴 ∧ 𝑆 hereditary 𝐴) → (𝑅 ∪ 𝑆) hereditary 𝐴) | ||
Theorem | snhesn 41820 | Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020.) |
⊢ {⟨𝐴, 𝐴⟩} hereditary {𝐵} | ||
Theorem | idhe 41821 | The identity relation is hereditary in any class. (Contributed by RP, 28-Mar-2020.) |
⊢ I hereditary 𝐴 | ||
Theorem | psshepw 41822 | 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 41823 | 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 41824 | 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 41825 | 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 41826 | Simplification of triple conjunction. Compare with simp2 1137. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜓))) | ||
Theorem | rp-simp2 41827 | Simplification of triple conjunction. Identical to simp2 1137. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
Theorem | rp-frege3g 41828 |
Add antecedent to ax-frege2 41825. More general statement than frege3 41829.
Like ax-frege2 41825, 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 41825 in Metamath. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))) | ||
Theorem | frege3 41829 | Add antecedent to ax-frege2 41825. Special case of rp-frege3g 41828. Proposition 3 of [Frege1879] p. 29. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → (𝜑 → 𝜓)) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | ||
Theorem | rp-misc1-frege 41830 | Double-use of ax-frege2 41825. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜓)) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | rp-frege24 41831 | Introducing an embedded antecedent. Alternate proof for frege24 41849. Closed form for a1d 25. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓))) | ||
Theorem | rp-frege4g 41832 | Deduction related to distribution. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))) | ||
Theorem | frege4 41833 | Special case of closed form of a2d 29. Special case of rp-frege4g 41832. Proposition 4 of [Frege1879] p. 31. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜑 → 𝜓))) → ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))) | ||
Theorem | frege5 41834 | 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 41835 | Distribute antecedent and add another. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜃 → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))) | ||
Theorem | rp-4frege 41836 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → ((𝜓 → 𝜑) → 𝜒)) → (𝜑 → 𝜒)) | ||
Theorem | rp-6frege 41837 | Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ((𝜓 → ((𝜒 → 𝜓) → 𝜃)) → (𝜓 → 𝜃))) | ||
Theorem | rp-8frege 41838 | Eliminate antecedent when it is implied by previous antecedent. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → ((𝜒 → 𝜓) → 𝜃))) → (𝜑 → (𝜓 → 𝜃))) | ||
Theorem | rp-frege25 41839 | Closed form for a1dd 50. Alternate route to Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
Theorem | frege6 41840 | 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 41841 |
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 41842 | 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 41843 | 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 41824, and ax-frege2 41825. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | frege26 41844 | Identical to idd 24. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜓)) | ||
Theorem | frege27 41845 | 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 41846 | Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 41834 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 41847 | A closed form of com23 86. Proposition 12 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃)))) | ||
Theorem | frege11 41848 | 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 41849 | Closed form for a1d 25. Deduction introducing an embedded antecedent. Identical to rp-frege24 41831 which was proved without relying on ax-frege8 41843. Proposition 24 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓))) | ||
Theorem | frege16 41850 | A closed form of com34 91. Proposition 16 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏))))) | ||
Theorem | frege25 41851 | Closed form for a1dd 50. Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒)))) | ||
Theorem | frege18 41852 | 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 41853 | A closed form of com45 97. Proposition 22 of [Frege1879] p. 41. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) → (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂)))))) | ||
Theorem | frege10 41854 | Result commuting antecedents within an antecedent. Proposition 10 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜃) → ((𝜓 → (𝜑 → 𝜒)) → 𝜃)) | ||
Theorem | frege17 41855 | A closed form of com3l 89. Proposition 17 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) | ||
Theorem | frege13 41856 | A closed form of com3r 87. Proposition 13 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃)))) | ||
Theorem | frege14 41857 | 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 41858 | A closed form of syl6 35. Proposition 19 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜒 → 𝜃) → (𝜑 → (𝜓 → 𝜃)))) | ||
Theorem | frege23 41859 | 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 41860 | A closed form of com4r 94. Proposition 15 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
Theorem | frege21 41861 | Replace antecedent in antecedent. Proposition 21 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜃) → ((𝜃 → 𝜓) → 𝜒))) | ||
Theorem | frege20 41862 | A closed form of syl8 76. Proposition 20 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜃 → 𝜏) → (𝜑 → (𝜓 → (𝜒 → 𝜏))))) | ||
Theorem | axfrege28 41863 | Contraposition. Identical to con3 153. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Axiom | ax-frege28 41864 | 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 41865 | Closed form of con3d 152. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → ¬ 𝜓))) | ||
Theorem | frege30 41866 | Commuted, closed form of con3d 152. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (¬ 𝜒 → ¬ 𝜑))) | ||
Theorem | axfrege31 41867 | Identical to notnotr 130. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) |
⊢ (¬ ¬ 𝜑 → 𝜑) | ||
Axiom | ax-frege31 41868 | 𝜑 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 41869 | Deduce con1 146 from con3 153. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → ¬ ¬ 𝜑)) → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))) | ||
Theorem | frege33 41870 | 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 41871 | 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 41872 | Commuted, closed form of con1d 145. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (¬ 𝜒 → (𝜑 → 𝜓))) | ||
Theorem | frege36 41873 | 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 41874 | If 𝜒 is a necessary consequence of the occurrence of 𝜓 or 𝜑, then 𝜒 is a necessary consequence of 𝜑 alone. Similar to a closed form of orcs 873. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜒)) | ||
Theorem | frege38 41875 | Identical to pm2.21 123. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
Theorem | frege39 41876 | 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 41877 | Anything implies pm2.18 128. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (¬ 𝜑 → ((¬ 𝜓 → 𝜓) → 𝜓)) | ||
Theorem | axfrege41 41878 | Identical to notnot 142. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 → ¬ ¬ 𝜑) | ||
Axiom | ax-frege41 41879 | 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 41880 | Not not id 22. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ¬ ¬ (𝜑 → 𝜑) | ||
Theorem | frege43 41881 | 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 41882 | Similar to a commuted pm2.62 898. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
Theorem | frege45 41883 | 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 41884 | 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 41885 | 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 41886 | 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 41998. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → ((𝜒 → 𝜃) → ((𝜓 → 𝜃) → (𝜑 → 𝜃)))) | ||
Theorem | frege49 41887 | Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → 𝜒))) | ||
Theorem | frege50 41888 | Closed form of jaoi 855. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((¬ 𝜑 → 𝜒) → 𝜓))) | ||
Theorem | frege51 41889 | Compare with jaod 857. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜒) → (𝜑 → ((¬ 𝜓 → 𝜃) → 𝜒)))) | ||
Here we leverage df-ifp 1062 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 41890 | Justification for ax-frege52a 41891. (Contributed by RP, 17-Apr-2020.) |
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒))) | ||
Axiom | ax-frege52a 41891 | 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 41892 | 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 41893 | Specialization of frege53a 41894. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (𝜑 → ((𝜑 ↔ 𝜓) → 𝜓)) | ||
Theorem | frege53a 41894 | Lemma for frege55a 41902. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ (if-(𝜑, 𝜃, 𝜒) → ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜃, 𝜒))) | ||
Theorem | axfrege54a 41895 | Justification for ax-frege54a 41896. Identical to biid 260. (Contributed by RP, 24-Dec-2019.) |
⊢ (𝜑 ↔ 𝜑) | ||
Axiom | ax-frege54a 41896 | Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 260. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜑) | ||
Theorem | frege54cor0a 41897 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑)) | ||
Theorem | frege54cor1a 41898 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ if-(𝜑, 𝜑, ¬ 𝜑) | ||
Theorem | frege55aid 41899 | Lemma for frege57aid 41906. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑)) | ||
Theorem | frege55lem1a 41900 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |