P. 450 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44901-45000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axfrege8 44901	Swap antecedents. Identical to pm2.04 91. This demonstrates that Axiom 8 of [Frege1879] p. 35 is redundant. Proof follows closely proof of pm2.04 91 in https://us.metamath.org/mmsolitaire/pmproofs.txt 91, 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 44902	A closed form of syl6 36. 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 44903	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 91 which can be proved from only ax-mp 5, ax-frege1 44884, and ax-frege2 44885. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	frege26 44904	Identical to idd 25. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜓))
Theorem	frege27 44905	We cannot (at the same time) affirm 𝜑 and deny 𝜑. Identical to id 23. Proposition 27 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → 𝜑)
Theorem	frege9 44906	Closed form of syl 18 with swapped antecedents. This proposition differs from frege5 44894 only in an unessential way. Identical to imim1 84. Proposition 9 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	frege12 44907	A closed form of com23 87. Proposition 12 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃))))
Theorem	frege11 44908	Elimination of a nested antecedent as a partial converse of ja 188. 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 107. Proposition 11 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	frege24 44909	Closed form for a1d 26. Deduction introducing an embedded antecedent. Identical to rp-frege24 44891 which was proved without relying on ax-frege8 44903. Proposition 24 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓)))
Theorem	frege16 44910	A closed form of com34 92. Proposition 16 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜓 → (𝜃 → (𝜒 → 𝜏)))))
Theorem	frege25 44911	Closed form for a1dd 51. Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜃 → 𝜒))))
Theorem	frege18 44912	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 44913	A closed form of com45 98. Proposition 22 of [Frege1879] p. 41. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) → (𝜑 → (𝜓 → (𝜒 → (𝜏 → (𝜃 → 𝜂))))))
Theorem	frege10 44914	Result commuting antecedents within an antecedent. Proposition 10 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜃) → ((𝜓 → (𝜑 → 𝜒)) → 𝜃))
Theorem	frege17 44915	A closed form of com3l 90. Proposition 17 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃))))
Theorem	frege13 44916	A closed form of com3r 88. Proposition 13 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃))))
Theorem	frege14 44917	Closed form of a deduction based on com3r 88. Proposition 14 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜑 → (𝜃 → (𝜓 → (𝜒 → 𝜏)))))
Theorem	frege19 44918	A closed form of syl6 36. Proposition 19 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜒 → 𝜃) → (𝜑 → (𝜓 → 𝜃))))
Theorem	frege23 44919	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 44920	A closed form of com4r 95. Proposition 15 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) → (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏)))))
Theorem	frege21 44921	Replace antecedent in antecedent. Proposition 21 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜃) → ((𝜃 → 𝜓) → 𝜒)))
Theorem	frege20 44922	A closed form of syl8 77. Proposition 20 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → ((𝜃 → 𝜏) → (𝜑 → (𝜓 → (𝜒 → 𝜏)))))
21.40.6.4  _Begriffsschrift_ Chapter II Implication and Negation
Theorem	axfrege28 44923	Contraposition. Identical to con3 154. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
Axiom	ax-frege28 44924	Contraposition. Identical to con3 154. 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 44925	Closed form of con3d 153. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → ¬ 𝜓)))
Theorem	frege30 44926	Commuted, closed form of con3d 153. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (¬ 𝜒 → ¬ 𝜑)))
Theorem	axfrege31 44927	Identical to notnotr 131. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.)
⊢ (¬ ¬ 𝜑 → 𝜑)
Axiom	ax-frege31 44928	𝜑 cannot be denied and (at the same time ) ¬ ¬ 𝜑 affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnotr 131. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ (¬ ¬ 𝜑 → 𝜑)
Theorem	frege32 44929	Deduce con1 147 from con3 154. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → ¬ ¬ 𝜑)) → ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)))
Theorem	frege33 44930	If 𝜑 or 𝜓 takes place, then 𝜓 or 𝜑 takes place. Identical to con1 147. Proposition 33 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑))
Theorem	frege34 44931	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 146. Proposition 34 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (𝜑 → (¬ 𝜒 → 𝜓)))
Theorem	frege35 44932	Commuted, closed form of con1d 146. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → (¬ 𝜒 → (𝜑 → 𝜓)))
Theorem	frege36 44933	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 125. Proposition 36 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
Theorem	frege37 44934	If 𝜒 is a necessary consequence of the occurrence of 𝜓 or 𝜑, then 𝜒 is a necessary consequence of 𝜑 alone. Similar to a closed form of orcs 889. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜑 → 𝜒))
Theorem	frege38 44935	Identical to pm2.21 124. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	frege39 44936	Syllogism between pm2.18 129 and pm2.24 125. Proposition 39 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → (¬ 𝜑 → 𝜓))
Theorem	frege40 44937	Anything implies pm2.18 129. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (¬ 𝜑 → ((¬ 𝜓 → 𝜓) → 𝜓))
Theorem	axfrege41 44938	Identical to notnot 143. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 → ¬ ¬ 𝜑)
Axiom	ax-frege41 44939	The affirmation of 𝜑 denies the denial of 𝜑. Identical to notnot 143. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ (𝜑 → ¬ ¬ 𝜑)
Theorem	frege42 44940	Not not id 23. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ¬ ¬ (𝜑 → 𝜑)
Theorem	frege43 44941	If there is a choice only between 𝜑 and 𝜑, then 𝜑 takes place. Identical to pm2.18 129. Proposition 43 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	frege44 44942	Similar to a commuted pm2.62 913. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜑))
Theorem	frege45 44943	Deduce pm2.6 193 from con1 147. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) → ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)))
Theorem	frege46 44944	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 193. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓))
Theorem	frege47 44945	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 44946	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 45058. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (¬ 𝜓 → 𝜒)) → ((𝜒 → 𝜃) → ((𝜓 → 𝜃) → (𝜑 → 𝜃))))
Theorem	frege49 44947	Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜒) → ((𝜓 → 𝜒) → 𝜒)))
Theorem	frege50 44948	Closed form of jaoi 871. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((¬ 𝜑 → 𝜒) → 𝜓)))
Theorem	frege51 44949	Compare with jaod 873. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜒) → (𝜑 → ((¬ 𝜓 → 𝜃) → 𝜒))))
21.40.6.5  _Begriffsschrift_ Chapter II with logical equivalence Here we leverage df-ifp 1079 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 44950	Justification for ax-frege52a 44951. (Contributed by RP, 17-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜃, 𝜒) → if-(𝜓, 𝜃, 𝜒)))
Axiom	ax-frege52a 44951	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 44952	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 218. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
Theorem	frege53aid 44953	Specialization of frege53a 44954. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝜑 → ((𝜑 ↔ 𝜓) → 𝜓))
Theorem	frege53a 44954	Lemma for frege55a 44962. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (if-(𝜑, 𝜃, 𝜒) → ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜃, 𝜒)))
Theorem	axfrege54a 44955	Justification for ax-frege54a 44956. Identical to biid 264. (Contributed by RP, 24-Dec-2019.)
⊢ (𝜑 ↔ 𝜑)
Axiom	ax-frege54a 44956	Reflexive equality of wffs. The content of 𝜑 is identical with the content of 𝜑. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 264. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜑)
Theorem	frege54cor0a 44957	Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜓 ↔ 𝜑) ↔ if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	frege54cor1a 44958	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	frege55aid 44959	Lemma for frege57aid 44966. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	frege55lem1a 44960	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜏 → if-(𝜓, 𝜑, ¬ 𝜑)) → (𝜏 → (𝜓 ↔ 𝜑)))
Theorem	frege55lem2a 44961	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	frege55a 44962	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	frege55cor1a 44963	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	frege56aid 44964	Lemma for frege57aid 44966. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) → ((𝜓 ↔ 𝜑) → (𝜑 → 𝜓)))
Theorem	frege56a 44965	Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))) → ((𝜓 ↔ 𝜑) → (if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃))))
Theorem	frege57aid 44966	This is the all important formula which allows to apply Frege-style definitions and explore their consequences. A closed form of biimpri 231. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
Theorem	frege57a 44967	Analogue of frege57aid 44966. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜓, 𝜒, 𝜃) → if-(𝜑, 𝜒, 𝜃)))
Theorem	axfrege58a 44968	Identical to anifp 1088. Justification for ax-frege58a 44969. (Contributed by RP, 28-Mar-2020.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Axiom	ax-frege58a 44969	If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2104. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒))
Theorem	frege58acor 44970	Lemma for frege59a 44971. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	frege59a 44971	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 44907 incorrectly referenced where frege30 44926 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (if-(𝜑, 𝜓, 𝜃) → (¬ if-(𝜑, 𝜒, 𝜏) → ¬ ((𝜓 → 𝜒) ∧ (𝜃 → 𝜏))))
Theorem	frege60a 44972	Swap antecedents of ax-frege58a 44969. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜓 → (𝜒 → 𝜃)) ∧ (𝜏 → (𝜂 → 𝜁))) → (if-(𝜑, 𝜒, 𝜂) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁))))
Theorem	frege61a 44973	Lemma for frege65a 44977. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜒) → 𝜃) → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	frege62a 44974	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2687 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 44975	Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (if-(𝜑, 𝜓, 𝜃) → (𝜂 → (((𝜓 → 𝜒) ∧ (𝜃 → 𝜏)) → if-(𝜑, 𝜒, 𝜏))))
Theorem	frege64a 44976	Lemma for frege65a 44977. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜒, 𝜂)) → (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜎, 𝜃, 𝜁))))
Theorem	frege65a 44977	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2687 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 44978	Swap antecedents of frege65a 44977. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ (((𝜒 → 𝜃) ∧ (𝜂 → 𝜁)) → (((𝜓 → 𝜒) ∧ (𝜏 → 𝜂)) → (if-(𝜑, 𝜓, 𝜏) → if-(𝜑, 𝜃, 𝜁))))
Theorem	frege67a 44979	Lemma for frege68a 44980. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
⊢ ((((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → (𝜓 ∧ 𝜒))) → (((𝜓 ∧ 𝜒) ↔ 𝜃) → (𝜃 → if-(𝜑, 𝜓, 𝜒))))
Theorem	frege68a 44980	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-(𝜑, 𝜓, 𝜒)))
21.40.6.6  _Begriffsschrift_ Chapter II with equivalence of sets
Theorem	axfrege52c 44981	Justification for ax-frege52c 44982. (Contributed by RP, 24-Dec-2019.)
⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜑 → [𝐵 / 𝑥]𝜑))
Axiom	ax-frege52c 44982	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 44983	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 44984	Lemma for frege102 (via frege92 45049). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → (𝑦 = 𝑧 → [𝑧 / 𝑥]𝜑))
Theorem	axfrege54c 44985	Reflexive equality of classes. Identical to eqid 2760. Justification for ax-frege54c 44986. (Contributed by RP, 24-Dec-2019.)
⊢ 𝐴 = 𝐴
Axiom	ax-frege54c 44986	Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2760. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
⊢ 𝐴 = 𝐴
Theorem	frege54b 44987	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 2760. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ 𝑥 = 𝑥
Theorem	frege54cor1b 44988	Reflexive equality. (Contributed by RP, 24-Dec-2019.)
⊢ [𝑥 / 𝑦]𝑦 = 𝑥
Theorem	frege55lem1b 44989*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
⊢ ((𝜑 → [𝑥 / 𝑦]𝑦 = 𝑧) → (𝜑 → 𝑥 = 𝑧))
Theorem	frege55lem2b 44990	Lemma for frege55b 44991. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
Theorem	frege55b 44991	Lemma for frege57b 44993. Proposition 55 of [Frege1879] p. 50. Note that eqtr2 2781 incorporates eqcom 2767 which is stronger than this proposition which is identical to equcomi 2049. 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.)
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
Theorem	frege56b 44992	Lemma for frege57b 44993. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ((𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) → (𝑦 = 𝑥 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)))
Theorem	frege57b 44993	Analogue of frege57aid 44966. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑))
Theorem	axfrege58b 44994	If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2104. Justification for ax-frege58b 44995. (Contributed by RP, 28-Mar-2020.)
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
Axiom	ax-frege58b 44995	If ∀𝑥𝜑 is affirmed, [𝑦 / 𝑥]𝜑 cannot be denied. Identical to stdpc4 2104. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
Theorem	frege58bid 44996	If ∀𝑥𝜑 is affirmed, 𝜑 cannot be denied. Identical to sp 2219. See ax-frege58b 44995 and frege58c 45015 for versions which more closely track the original. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.)
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	frege58bcor 44997	Lemma for frege59b 44998. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	frege59b 44998	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 44907 incorrectly referenced where frege30 44926 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → (¬ [𝑦 / 𝑥]𝜓 → ¬ ∀𝑥(𝜑 → 𝜓)))
Theorem	frege60b 44999	Swap antecedents of ax-frege58b 44995. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → ([𝑦 / 𝑥]𝜓 → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜒)))
Theorem	frege61b 45000	Lemma for frege65b 45004. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
⊢ (([𝑥 / 𝑦]𝜑 → 𝜓) → (∀𝑦𝜑 → 𝜓))