P. 365 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36401-36500   *Has distinct variable group(s)

Type	Label	Description
Statement
21.25.3.4  _Begriffsschrift_ Chapter II Implication and Negation
Theorem	axfrege28 36401	Contraposition. Identical to con3 140. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
Axiom	ax-frege28 36402	Contraposition. Identical to con3 140. Theorem *2.16 of [WhiteheadRussell] p. 103. Axiom 28 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
Theorem	frege29 36403	Closed form of con3d 139. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( -. ch -> -. ps ) ) )
Theorem	frege30 36404	Commuted, closed form of con3d 139. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( -. ch -> -. ph ) ) )
Theorem	axfrege31 36405	Identical to notnot2 116. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.)
|- ( -. -. ph -> ph )
Axiom	ax-frege31 36406	ph cannot be denied and (at the same time ) -. -. ph affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnot2 116. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( -. -. ph -> ph )
Theorem	frege32 36407	Deduce con1 132 from con3 140. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ( -. ps -> -. -. ph ) ) -> ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) )
Theorem	frege33 36408	If ph or ps takes place, then ps or ph takes place. Identical to con1 132. Proposition 33 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( -. ps -> ph ) )
Theorem	frege34 36409	If as a conseqence of the occurence of the circumstance ph, when the obstacle ps is removed, ch takes place, then from the circumstance that ch does not take place while ph occurs the occurence of the obstacle ps can be inferred. Closed form of con1d 128. Proposition 34 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( ph -> ( -. ch -> ps ) ) )
Theorem	frege35 36410	Commuted, closed form of con1d 128. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( -. ch -> ( ph -> ps ) ) )
Theorem	frege36 36411	The case in which ps is denied, -. ph is affirmed, and ph is affirmed does not occur. If ph occurs, then (at least) one of the two, ph or ps, takes place (no matter what ps might be). Identical to pm2.24 113. Proposition 36 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( -. ph -> ps ) )
Theorem	frege37 36412	If ch is a necessary consequence of the occurrence of ps or ph, then ch is a necessary consequence of ph alone. Similar to a closed form of orcs 396. Proposition 37 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ch ) -> ( ph -> ch ) )
Theorem	frege38 36413	Identical to pm2.21 112. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( -. ph -> ( ph -> ps ) )
Theorem	frege39 36414	Syllogism between pm2.18 114 and pm2.24 113. Proposition 39 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ph ) -> ( -. ph -> ps ) )
Theorem	frege40 36415	Anything implies pm2.18 114. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( -. ph -> ( ( -. ps -> ps ) -> ps ) )
Theorem	axfrege41 36416	Identical to notnot1 126. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> -. -. ph )
Axiom	ax-frege41 36417	The affirmation of ph denies the denial of ph. Identical to notnot1 126. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ph -> -. -. ph )
Theorem	frege42 36418	Not not id 23. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- -. -. ( ph -> ph )
Theorem	frege43 36419	If there is a choice only between ph and ph, then ph takes place. Identical to pm2.18 114. Proposition 43 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ph ) -> ph )
Theorem	frege44 36420	Similar to a commuted pm2.62 411. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ps -> ph ) -> ph ) )
Theorem	frege45 36421	Deduce pm2.6 174 from con1 132. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( -. ph -> ps ) -> ( -. ps -> ph ) ) -> ( ( -. ph -> ps ) -> ( ( ph -> ps ) -> ps ) ) )
Theorem	frege46 36422	If ps holds when ph occurs as well as when ph does not occur, then ps holds. If ps or ph occurs and if the occurences of ph has ps as a necessary consequence, then ps takes place. Identical to pm2.6 174. Proposition 46 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ph -> ps ) -> ps ) )
Theorem	frege47 36423	Deduce consequence follows from either path implied by a disjunction. If ph, as well as ps is sufficient condition for ch and ps or ph takes place, then the proposition ch holds. Proposition 47 of [Frege1879] p. 48. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ps -> ch ) -> ( ( ph -> ch ) -> ch ) ) )
Theorem	frege48 36424	Closed form of syllogism with internal disjunction. If ph is a sufficient condition for the occurence of ch or ps and if ch, as well as ps, is a sufficient condition for th, then ph is a sufficient condition for th. See application in frege101 36536. Proposition 48 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( -. ps -> ch ) ) -> ( ( ch -> th ) -> ( ( ps -> th ) -> ( ph -> th ) ) ) )
Theorem	frege49 36425	Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( -. ph -> ps ) -> ( ( ph -> ch ) -> ( ( ps -> ch ) -> ch ) ) )
Theorem	frege50 36426	Closed form of jaoi 381. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ps ) -> ( ( ch -> ps ) -> ( ( -. ph -> ch ) -> ps ) ) )
Theorem	frege51 36427	Compare with jaod 382. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( th -> ch ) -> ( ph -> ( ( -. ps -> th ) -> ch ) ) ) )
21.25.3.5  _Begriffsschrift_ Chapter II with logical equivalence Here we leverage df-ifp 1422 to partition a wff into two that are disjoint with the selector wff. Thus if we are given |- ( ph <-> if- ( ps , ch , th ) ) then we replace the concept (illegal in our notation ) ( ph ` ps ) with if- ( ps , ch , th ) to reason about the values of the "function." Likewise, we replace the similarly illegal concept A. ps ph with ( ch /\ th ).
Theorem	axfrege52a 36428	Justification for ax-frege52a 36429. (Contributed by RP, 17-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
Axiom	ax-frege52a 36429	The case when the content of ph is identical with the content of ps and in which a proposition controlled by an element for which we substitute the content of ph is affirmed ( in this specific case the identity logical funtion ) and the same proposition, this time where we subsituted the content of ps, is denied does not take place. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
Theorem	frege52aid 36430	The case when the content of ph is identical with the content of ps and in which ph is affirmed and ps is denied does not take place. Identical to biimp 197. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ph -> ps ) )
Theorem	frege53aid 36431	Specialization of frege53a 36432. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ph -> ( ( ph <-> ps ) -> ps ) )
Theorem	frege53a 36432	Lemma for frege55a 36440. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- (if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )
Theorem	axfrege54a 36433	Justification for ax-frege54a 36434. Identical to biid 240. (Contributed by RP, 24-Dec-2019.)
|- ( ph <-> ph )
Axiom	ax-frege54a 36434	Reflexive equality of wffs. The content of ph is identical with the content of ph. Part of Axiom 54 of [Frege1879] p. 50. Identical to biid 240. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( ph <-> ph )
Theorem	frege54cor0a 36435	Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ps <-> ph ) <-> if- ( ps , ph , -. ph ) )
Theorem	frege54cor1a 36436	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- if- ( ph , ph , -. ph )
Theorem	frege55aid 36437	Lemma for frege57aid 36444. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph <-> ps ) -> ( ps <-> ph ) )
Theorem	frege55lem1a 36438	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ta -> if- ( ps , ph , -. ph ) ) -> ( ta -> ( ps <-> ph ) ) )
Theorem	frege55lem2a 36439	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )
Theorem	frege55a 36440	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )
Theorem	frege55cor1a 36441	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ps <-> ph ) )
Theorem	frege56aid 36442	Lemma for frege57aid 36444. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( ph <-> ps ) -> ( ph -> ps ) ) -> ( ( ps <-> ph ) -> ( ph -> ps ) ) )
Theorem	frege56a 36443	Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( ph <-> ps ) -> (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) ) -> ( ( ps <-> ph ) -> (if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) ) )
Theorem	frege57aid 36444	This is the all imporant formula which allows us to apply Frege-style definitions and explore their consequences. A closed form of biimpri 210. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> ( ps -> ph ) )
Theorem	frege57a 36445	Analogue of frege57aid 36444. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ph <-> ps ) -> (if- ( ps , ch , th ) -> if- ( ph , ch , th ) ) )
Theorem	axfrege58a 36446	Identical to anifp 1429. Justification for ax-frege58a 36447. (Contributed by RP, 28-Mar-2020.)
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
Axiom	ax-frege58a 36447	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2152. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
Theorem	frege58acor 36448	Lemma for frege59a 36449. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> (if- ( ph , ps , th ) -> if- ( ph , ch , ta ) ) )
Theorem	frege59a 36449	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 36385 incorrectly referenced where frege30 36404 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- (if- ( ph , ps , th ) -> ( -. if- ( ph , ch , ta ) -> -. ( ( ps -> ch ) /\ ( th -> ta ) ) ) )
Theorem	frege60a 36450	Swap antecedents of ax-frege58a 36447. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ( ch -> th ) ) /\ ( ta -> ( et -> ze ) ) ) -> (if- ( ph , ch , et ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege61a 36451	Lemma for frege65a 36455. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( (if- ( ph , ps , ch ) -> th ) -> ( ( ps /\ ch ) -> th ) )
Theorem	frege62a 36452	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 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- ( ph , ps , th ) -> ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> if- ( ph , ch , ta ) ) )
Theorem	frege63a 36453	Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- (if- ( ph , ps , th ) -> ( et -> ( ( ( ps -> ch ) /\ ( th -> ta ) ) -> if- ( ph , ch , ta ) ) ) )
Theorem	frege64a 36454	Lemma for frege65a 36455. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( (if- ( ph , ps , ta ) -> if- ( si , ch , et ) ) -> ( ( ( ch -> th ) /\ ( et -> ze ) ) -> (if- ( ph , ps , ta ) -> if- ( si , th , ze ) ) ) )
Theorem	frege65a 36455	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ps -> ch ) /\ ( ta -> et ) ) -> ( ( ( ch -> th ) /\ ( et -> ze ) ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege66a 36456	Swap antecedents of frege65a 36455. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ch -> th ) /\ ( et -> ze ) ) -> ( ( ( ps -> ch ) /\ ( ta -> et ) ) -> (if- ( ph , ps , ta ) -> if- ( ph , th , ze ) ) ) )
Theorem	frege67a 36457	Lemma for frege68a 36458. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.)
|- ( ( ( ( ps /\ ch ) <-> th ) -> ( th -> ( ps /\ ch ) ) ) -> ( ( ( ps /\ ch ) <-> th ) -> ( th -> if- ( ph , ps , ch ) ) ) )
Theorem	frege68a 36458	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.)
|- ( ( ( ps /\ ch ) <-> th ) -> ( th -> if- ( ph , ps , ch ) ) )
21.25.3.6  _Begriffsschrift_ Chapter II with equivalence of sets
Theorem	axfrege52c 36459	Justification for ax-frege52c 36460. (Contributed by RP, 24-Dec-2019.)
|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )
Axiom	ax-frege52c 36460	One side of dfsbcq 3307. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )
Theorem	frege52b 36461	The case when the content of x is identical with the content of y and in which a proposition controlled by an element for which we substitute the content of x is affirmed and the same proposition, this time where we subsitute the content of y, is denied does not take place. In [ x / z ] ph, x can also occur in other than the argument ( z) places. Hence x may still be contained in [ y / z ] ph. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
Theorem	frege53b 36462	Lemma for frege102 (via frege92 36527). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( x = z -> [ z / y ] ph ) )
Theorem	axfrege54c 36463	Reflexive equality of classes. Identical to eqid 2423. Justification for ax-frege54c 36464. (Contributed by RP, 24-Dec-2019.)
|- A = A
Axiom	ax-frege54c 36464	Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2423. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)
|- A = A
Theorem	frege54b 36465	Reflexive equality of sets. The content of x is identical with the content of x. Part of Axiom 54 of [Frege1879] p. 50. Slightly specialized version of eqid 2423. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- x = x
Theorem	frege54cor1b 36466	Reflexive equality. (Contributed by RP, 24-Dec-2019.)
|- [ x / y ] y = x
Theorem	frege55lem1b 36467*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> [ x / y ] y = z ) -> ( ph -> x = z ) )
Theorem	frege55lem2b 36468	Lemma for frege55b 36469. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> [ y / z ] z = x )
Theorem	frege55b 36469	Lemma for frege57b 36471. Proposition 55 of [Frege1879] p. 50. Note that eqtr2 2450 incorporates eqcom 2432 which is stronger than this proposition which is identical to equcomi 1848. Is is possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> y = x )
Theorem	frege56b 36470	Lemma for frege57b 36471. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) ) -> ( y = x -> ( [ x / z ] ph -> [ y / z ] ph ) ) )
Theorem	frege57b 36471	Analogue of frege57aid 36444. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
Theorem	axfrege58b 36472	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2152. Justification for ax-frege58b 36473. (Contributed by RP, 28-Mar-2020.)
|- ( A. x ph -> [ y / x ] ph )
Axiom	ax-frege58b 36473	If A. x ph is affirmed, [ y / x ] ph cannot be denied. Identical to stdpc4 2152. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (New usage is discouraged.)
|- ( A. x ph -> [ y / x ] ph )
Theorem	frege58bid 36474	If A. x ph is affirmed, ph cannot be denied. Identical to sp 1915. See ax-frege58b 36473 and frege58c 36493 for versions which more closely track the original. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 28-Mar-2020.) (Proof modification is discouraged.)
|- ( A. x ph -> ph )
Theorem	frege58bcor 36475	Lemma for frege59b 36476. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	frege59b 36476	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 36385 incorrectly referenced where frege30 36404 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( -. [ x / y ] ps -> -. A. y ( ph -> ps ) ) )
Theorem	frege60b 36477	Swap antecedents of ax-frege58b 36473. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ps -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege61b 36478	Lemma for frege65b 36482. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> ps ) -> ( A. y ph -> ps ) )
Theorem	frege62b 36479	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( A. y ( ph -> ps ) -> [ x / y ] ps ) )
Theorem	frege63b 36480	Lemma for frege91 36526. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [ x / y ] ph -> ( ps -> ( A. y ( ph -> ch ) -> [ x / y ] ch ) ) )
Theorem	frege64b 36481	Lemma for frege65b 36482. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( [ x / y ] ph -> [ z / y ] ps ) -> ( A. y ( ps -> ch ) -> ( [ x / y ] ph -> [ z / y ] ch ) ) )
Theorem	frege65b 36482	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. In Frege care is taken to point out that the variables in the first clauses are independent of each other and of the final term so another valid translation could be : |- ( A. x ( [ x / a ] ph -> [ x / b ] ps ) -> ( A. y ( [ y / b ] ps -> [ y / c ] ch ) -> ( [ z / a ] ph -> [ z / c ] ch ) ) ). But that is perhaps too pedantic a translation for this exploration. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [ y / x ] ph -> [ y / x ] ch ) ) )
Theorem	frege66b 36483	Swap antecedents of frege65b 36482. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( A. x ( ph -> ps ) -> ( A. x ( ch -> ph ) -> ( [ y / x ] ch -> [ y / x ] ps ) ) )
Theorem	frege67b 36484	Lemma for frege68b 36485. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( ( A. x ph <-> ps ) -> ( ps -> A. x ph ) ) -> ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) ) )
Theorem	frege68b 36485	Combination of applying a definition and applying it to a specific instance. Proposition 68 of [Frege1879] p. 54. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( ( A. x ph <-> ps ) -> ( ps -> [ y / x ] ph ) )
21.25.3.7  _Begriffsschrift_ Chapter II with equivalence of classes (where they are sets)
Theorem	frege53c 36486	Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( [. A / x ]. ph -> ( A = B -> [. B / x ]. ph ) )
Theorem	frege54cor1c 36487*	Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Revised by RP, 25-Apr-2020.)
|- A e. C   =>    |- [. A / x ]. x = A
Theorem	frege55lem1c 36488*	Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.)
|- ( ( ph -> [. A / x ]. x = B ) -> ( ph -> A = B ) )
Theorem	frege55lem2c 36489*	Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> [. A / z ]. z = x )
Theorem	frege55c 36490	Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- ( x = A -> A = x )
Theorem	frege56c 36491*	Lemma for frege57c 36492. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- B e. C   =>    |- ( ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) -> ( B = A -> ( [. A / x ]. ph -> [. B / x ]. ph ) ) )
Theorem	frege57c 36492*	Swap order of implication in ax-frege52c 36460. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. C   =>    |- ( A = B -> ( [. B / x ]. ph -> [. A / x ]. ph ) )
Theorem	frege58c 36493	Principle related to sp 1915. Axiom 58 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ph -> [. A / x ]. ph )
Theorem	frege59c 36494	A kind of Aristotelian inference. 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 36385 incorrectly referenced where frege30 36404 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( -. [. A / x ]. ps -> -. A. x ( ph -> ps ) ) )
Theorem	frege60c 36495	Swap antecedents of frege58c 36493. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ( ps -> ch ) ) -> ( [. A / x ]. ps -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege61c 36496	Lemma for frege65c 36500. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. A / x ]. ph -> ps ) -> ( A. x ph -> ps ) )
Theorem	frege62c 36497	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 when the minor premise has a particular context. Proposition 62 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( A. x ( ph -> ps ) -> [. A / x ]. ps ) )
Theorem	frege63c 36498	Analogue of frege63b 36480. Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( [. A / x ]. ph -> ( ps -> ( A. x ( ph -> ch ) -> [. A / x ]. ch ) ) )
Theorem	frege64c 36499	Lemma for frege65c 36500. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( ( [. C / x ]. ph -> [. A / x ]. ps ) -> ( A. x ( ps -> ch ) -> ( [. C / x ]. ph -> [. A / x ]. ch ) ) )
Theorem	frege65c 36500	A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2363 when the minor premise has a general context. Proposition 65 of [Frege1879] p. 53. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|- A e. B   =>    |- ( A. x ( ph -> ps ) -> ( A. x ( ps -> ch ) -> ( [. A / x ]. ph -> [. A / x ]. ch ) ) )