HomeTheorem List (p. 382 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 382 of 426) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | axfrege8 38101 |
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 http://us.metamath.org/mmsolitaire/pmproofs.txt, 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 38102 | 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 38103 | 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 38084, and ax-frege2 38085. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
|
| ||
| Theorem | frege26 38104 | Identical to idd 24. Proposition 26 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| | ||
| Theorem | frege27 38105 |
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 38106 | Closed form of syl 17 with swapped antecedents. This proposition differs from frege5 38094 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 38107 | A closed form of com23 86. Proposition 12 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege11 38108 |
Elimination of a nested antecedent as a partial converse of ja 173. 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 38109 | Closed form for a1d 25. Deduction introducing an embedded antecedent. Identical to rp-frege24 38091 which was proved without relying on ax-frege8 38103. Proposition 24 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege16 38110 | A closed form of com34 91. Proposition 16 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ||
| Theorem | frege25 38111 | Closed form for a1dd 50. Proposition 25 of [Frege1879] p. 42. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege18 38112 | 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 38113 | A closed form of com45 97. Proposition 22 of [Frege1879] p. 41. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| ||
| Theorem | frege10 38114 | Result commuting antecedents within an antecedent. Proposition 10 of [Frege1879] p. 36. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege17 38115 | A closed form of com3l 89. Proposition 17 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege13 38116 | A closed form of com3r 87. Proposition 13 of [Frege1879] p. 37. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege14 38117 | 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 38118 | A closed form of syl6 35. Proposition 19 of [Frege1879] p. 39. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege23 38119 | 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 38120 | A closed form of com4r 94. Proposition 15 of [Frege1879] p. 38. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege21 38121 | Replace antecedent in antecedent. Proposition 21 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege20 38122 | A closed form of syl8 76. Proposition 20 of [Frege1879] p. 40. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | axfrege28 38123 | Contraposition. Identical to con3 149. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by RP, 24-Dec-2019.) |
 | ||
| Axiom | ax-frege28 38124 | Contraposition. Identical to con3 149. 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 38125 | Closed form of con3d 148. Proposition 29 of [Frege1879] p. 43. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege30 38126 | Commuted, closed form of con3d 148. Proposition 30 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | axfrege31 38127 | Identical to notnotr 125. Axiom 31 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) |
|
| ||
| Axiom | ax-frege31 38128 |
cannot be
denied and (at the same time ) affirmed.
Duplex negatio affirmat. The denial of the denial is affirmation.
Identical to notnotr 125. Axiom 31 of [Frege1879] p. 44. (Contributed by
RP, 24-Dec-2019.) (New usage is discouraged.)
|
|
| ||
| Theorem | frege32 38129 | Deduce con1 143 from con3 149. Proposition 32 of [Frege1879] p. 44. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege33 38130 |
If or takes place, then or takes place.
Identical to con1 143. Proposition 33 of [Frege1879] p. 44. (Contributed
by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | frege34 38131 |
If as a conseqence of the occurence of the circumstance , when the
obstacle is
removed, takes
place, then from the circumstance
that does not
take place while occurs the occurence of the
obstacle can
be inferred. Closed form of con1d 139. Proposition 34
of [Frege1879] p. 45. (Contributed by
RP, 24-Dec-2019.)
(Proof modification is discouraged.)
|
|
| ||
| Theorem | frege35 38132 | Commuted, closed form of con1d 139. Proposition 35 of [Frege1879] p. 45. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege36 38133 |
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 121. Proposition 36 of [Frege1879] p. 45.
(Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
| | ||
| Theorem | frege37 38134 |
If is a necessary
consequence of the occurrence of or
, then is a necessary
consequence of
alone. Similar
to a closed form of orcs 409. Proposition 37 of [Frege1879] p. 46.
(Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
| | ||
| Theorem | frege38 38135 | Identical to pm2.21 120. Proposition 38 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege39 38136 | Syllogism between pm2.18 122 and pm2.24 121. Proposition 39 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege40 38137 | Anything implies pm2.18 122. Proposition 40 of [Frege1879] p. 46. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | axfrege41 38138 | Identical to notnot 136. Axiom 41 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) |
|
| ||
| Axiom | ax-frege41 38139 |
The affirmation of denies the denial of . Identical to
notnot 136. Axiom 41 of [Frege1879] p. 47. (Contributed by RP,
24-Dec-2019.) (New usage is discouraged.)
|
|
| ||
| Theorem | frege42 38140 | Not not id 22. Proposition 42 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| | ||
| Theorem | frege43 38141 |
If there is a choice only between and , then takes
place. Identical to pm2.18 122. Proposition 43 of [Frege1879] p. 47.
(Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | frege44 38142 | Similar to a commuted pm2.62 425. Proposition 44 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege45 38143 | Deduce pm2.6 182 from con1 143. Proposition 45 of [Frege1879] p. 47. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege46 38144 |
If holds when occurs as well as
when does not
occur,
then holds.
If or occurs and if the
occurences of
has as a necessary
consequence, then
takes place.
Identical to pm2.6 182. Proposition 46 of [Frege1879] p. 48. (Contributed
by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | frege47 38145 |
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 38146 |
Closed form of syllogism with internal disjunction. If is a
sufficient condition for the occurence of or and if ,
as well as ,
is a sufficient condition for , then is
a sufficient condition for . See application in frege101 38258.
Proposition 48 of [Frege1879] p. 49.
(Contributed by RP, 24-Dec-2019.)
(Proof modification is discouraged.)
|
|
| ||
| Theorem | frege49 38147 | Closed form of deduction with disjunction. Proposition 49 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege50 38148 | Closed form of jaoi 394. Proposition 50 of [Frege1879] p. 49. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege51 38149 | Compare with jaod 395. Proposition 51 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
Here we leverage df-ifp 1013 to partition a wff into two that are disjoint with the selector wff.
Thus if we are given | ||
| Theorem | axfrege52a 38150 | Justification for ax-frege52a 38151. (Contributed by RP, 17-Apr-2020.) |
 if-
if- | ||
| Axiom | ax-frege52a 38151 |
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 funtion ) 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 38152 |
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 205. Part of Axiom 52 of [Frege1879] p. 50.
(Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)
|
|
| ||
| Theorem | frege53aid 38153 | Specialization of frege53a 38154. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| | ||
| Theorem | frege53a 38154 | Lemma for frege55a 38162. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| if-
if- | ||
| Theorem | axfrege54a 38155 | Justification for ax-frege54a 38156. Identical to biid 251. (Contributed by RP, 24-Dec-2019.) |
| | ||
| Axiom | ax-frege54a 38156 |
Reflexive equality of wffs. The content of is identical with the
content of . Part of Axiom 54 of [Frege1879] p. 50. Identical to
biid 251. (Contributed by RP, 24-Dec-2019.)
(New usage is discouraged.)
|
| | ||
| Theorem | frege54cor0a 38157 | Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| if- | ||
| Theorem | frege54cor1a 38158 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| if- | ||
| Theorem | frege55aid 38159 | Lemma for frege57aid 38166. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) |
|
| ||
| Theorem | frege55lem1a 38160 | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| if- | ||
| Theorem | frege55lem2a 38161 | Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
if- | ||
| Theorem | frege55a 38162 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
if- | ||
| Theorem | frege55cor1a 38163 | Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege56aid 38164 | Lemma for frege57aid 38166. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| | ||
| Theorem | frege56a 38165 | Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| if-
if- if-
if- | ||
| Theorem | frege57aid 38166 | This is the all imporant formula which allows us to apply Frege-style definitions and explore their consequences. A closed form of biimpri 218. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege57a 38167 | Analogue of frege57aid 38166. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
if-
if- | ||
| Theorem | axfrege58a 38168 | Identical to anifp 1020. Justification for ax-frege58a 38169. (Contributed by RP, 28-Mar-2020.) |
![/\](wedge.gif "/\"){kind=small} if- | ||
| Axiom | ax-frege58a 38169 |
If   is affirmed,    ![]](rbrack.gif "]"){kind=small} cannot be denied. Identical
to stdpc4 2353. Axiom 58 of [Frege1879] p. 51. (Contributed by RP,
28-Mar-2020.) (New usage is discouraged.)
|
| if- | ||
| Theorem | frege58acor 38170 | Lemma for frege59a 38171. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if- if- | ||
| Theorem | frege59a 38171 |
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 38107 incorrectly referenced where frege30 38126 is in the original. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if-
if-
| ||
| Theorem | frege60a 38172 | Swap antecedents of ax-frege58a 38169. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
 if-
if-
if- | ||
| Theorem | frege61a 38173 | Lemma for frege65a 38177. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if-
| ||
| Theorem | frege62a 38174 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2563 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 38175 | Proposition 63 of [Frege1879] p. 52. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if-
if- | ||
| Theorem | frege64a 38176 | Lemma for frege65a 38177. Proposition 64 of [Frege1879] p. 53. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
if- if- if- if- | ||
| Theorem | frege65a 38177 | A kind of Aristotelian inference. This judgement replaces the mode of inference barbara 2563 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 38178 | Swap antecedents of frege65a 38177. Proposition 66 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if- if- | ||
| Theorem | frege67a 38179 | Lemma for frege68a 38180. Proposition 67 of [Frege1879] p. 54. (Contributed by RP, 17-Apr-2020.) (Proof modification is discouraged.) |
| if- | ||
| Theorem | frege68a 38180 | 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 38181 | Justification for ax-frege52c 38182. (Contributed by RP, 24-Dec-2019.) |
 
  ![].](_drbrack.gif "]."){kind=small} | ||
| Axiom | ax-frege52c 38182 | One side of dfsbcq 3437. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
|
| ||
| Theorem | frege52b 38183 |
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 38184 | Lemma for frege102 (via frege92 38249). Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | axfrege54c 38185 | Reflexive equality of classes. Identical to eqid 2622. Justification for ax-frege54c 38186. (Contributed by RP, 24-Dec-2019.) |
| | ||
| Axiom | ax-frege54c 38186 | Reflexive equality of sets (as classes). Part of Axiom 54 of [Frege1879] p. 50. Identical to eqid 2622. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.) |
| | ||
| Theorem | frege54b 38187 |
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 2622. (Contributed by RP, 24-Dec-2019.)
(Proof modification is discouraged.)
|
| | ||
| Theorem | frege54cor1b 38188 | Reflexive equality. (Contributed by RP, 24-Dec-2019.) |
| | ||
| Theorem | frege55lem1b 38189* | Necessary deduction regarding substitution of value in equality. (Contributed by RP, 24-Dec-2019.) |
|
| ||
| Theorem | frege55lem2b 38190 | Lemma for frege55b 38191. Core proof of Proposition 55 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege55b 38191 |
Lemma for frege57b 38193. Proposition 55 of [Frege1879] p. 50.
Note that eqtr2 2642 incorporates eqcom 2629 which is stronger than this proposition which is identical to equcomi 1944. 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.) |
|
| ||
| Theorem | frege56b 38192 | Lemma for frege57b 38193. Proposition 56 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege57b 38193 | Analogue of frege57aid 38166. Proposition 57 of [Frege1879] p. 51. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | axfrege58b 38194 |
If is affirmed, cannot be denied.
Identical to stdpc4 2353. Justification for ax-frege58b 38195. (Contributed
by RP, 28-Mar-2020.)
|
| | ||
| Axiom | ax-frege58b 38195 |
If is affirmed, cannot be denied.
Identical to stdpc4 2353. Axiom 58 of [Frege1879] p. 51. (Contributed by
RP, 28-Mar-2020.) (New usage is discouraged.)
|
| | ||
| Theorem | frege58bid 38196 |
If is affirmed, cannot be denied. Identical to sp 2053.
See ax-frege58b 38195 and frege58c 38215 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 38197 | Lemma for frege59b 38198. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege59b 38198 |
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 38107 incorrectly referenced where frege30 38126 is in the original. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege60b 38199 | Swap antecedents of ax-frege58b 38195. Proposition 60 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
|
| ||
| Theorem | frege61b 38200 | Lemma for frege65b 38204. Proposition 61 of [Frege1879] p. 52. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.) |
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |
