Home | Metamath
Proof ExplorerTheorem List
(p. 280 of 321)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22283) |
Hilbert Space Explorer
(22284-23806) |
Users' Mathboxes
(23807-32095) |

Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | ||||||||||||||||||||||||||||||||

Theorem | ad4ant14 27901 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant123 27902 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant124 27903 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant134 27904 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant23 27905 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant24 27906 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad4ant234 27907 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant12 27908 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant13 27909 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant14 27910 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant15 27911 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant23 27912 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant24 27913 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant25 27914 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant245 27915 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant234 27916 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant235 27917 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant123 27918 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant124 27919 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant125 27920 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant134 27921 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant135 27922 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant145 27923 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant1345 27924 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

Theorem | ad5ant2345 27925 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) | ||||||||||||||||||||||||||||||

19.24.2 Supplementary unification
deductions | ||||||||||||||||||||||||||||||||

Theorem | biimp 27926 | Importation inference similar to imp 419, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi2imp 27927 | Importation inference similar to imp 419, except the both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi3impb 27928 | Similar to 3impb 1149 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi3impa 27929 | Similar to 3impa 1148 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi23impib 27930 | 3impib 1151 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi13impib 27931 | 3impib 1151 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi123impib 27932 | 3impib 1151 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi13impia 27933 | 3impia 1150 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi123impia 27934 | 3impia 1150 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi33imp12 27935 | 3imp 1147 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi23imp13 27936 | 3imp 1147 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi13imp23 27937 | 3imp 1147 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi13imp2 27938 | Similar to 3imp 1147 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi12imp3 27939 | Similar to 3imp 1147 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi23imp1 27940 | Similar to 3imp 1147 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

Theorem | bi123imp0 27941 | Similar to 3imp 1147 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||

19.24.3 Conventional Metamath proofs, some
derived from VD proofs | ||||||||||||||||||||||||||||||||

Theorem | iidn3 27942 | idn3 28073 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee222 27943 | e222 28094 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee3bir 27944 | Right-biconditional form of e3 28206 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee13 27945 | e13 28217 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee121 27946 | e121 28114 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee122 27947 | e122 28111 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee333 27948 | e333 28202 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee323 27949 | e323 28235 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3ornot23 27950 | If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 28316. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | orbi1r 27951 | orbi1 687 with order of disjuncts reversed. Derived from orbi1rVD 28317. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | bitr3 27952 | Closed nested implication form of bitr3i 243. Derived automatically from bitr3VD 28318. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3orbi123 27953 | pm4.39 842 with a 3-conjunct antecedent. This proof is 3orbi123VD 28319 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | syl5imp 27954 | Closed form of syl5 30. Derived automatically from syl5impVD 28332. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | impexp3a 27955 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. After the
User's Proof was completed, it was minimized. The completed User's Proof
before minimization is not shown. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | com3rgbi 27956 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | impexp3acom3r 27957 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual Deduction Proof (not shown) was minimized. The
minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | ee1111 27958 |
Non-virtual deduction form of e1111 28133. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | pm2.43bgbi 27959 |
Logical equivalence of a 2-left-nested implication and a 1-left-nested
implicated
when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||

Theorem | pm2.43cbi 27960 |
Logical equivalence of a 3-left-nested implication and a 2-left-nested
implicated when two antecedents of the former implication are identical.
(Contributed by Alan Sare, 18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is
a Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. The completed Virtual Deduction Proof (not
shown) was minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | ee233 27961 |
Non-virtual deduction form of e233 28234. (Contributed by Alan Sare,
18-Mar-2012.)
(Proof modification is discouraged.) (New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The
completed Virtual
Deduction Proof (not shown) was minimized. The minimized proof is
shown.
| ||||||||||||||||||||||||||||||

Theorem | imbi12 27962 | Implication form of imbi12i 317. imbi12 27962 is imbi12VD 28342 without virtual deductions and was automatically derived from imbi12VD 28342 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | imbi13 27963 | Join three logical equivalences to form equivalence of implications. imbi13 27963 is imbi13VD 28343 without virtual deductions and was automatically derived from imbi13VD 28343 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ee33 27964 |
Non-virtual deduction form of e33 28203. (Contributed by Alan Sare,
18-Mar-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. The completed Virtual Deduction Proof (not shown) was
minimized. The minimized proof is shown.
| ||||||||||||||||||||||||||||||

Theorem | con5 27965 | Bi-conditional contraposition variation. This proof is con5VD 28369 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | con5i 27966 | Inference form of con5 27965. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | exlimexi 27967 | Inference similar to Theorem 19.23 of [Margaris] p. 90. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sb5ALT 27968* | Equivalence for substitution. Alternate proof of sb5 2147. This proof is sb5ALTVD 28382 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | eexinst01 27969 | exinst01 28083 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | eexinst11 27970 | exinst11 28084 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | vk15.4j 27971 | Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 27971 is vk15.4jVD 28383 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | notnot2ALT 27972 | Converse of double negation. Alternate proof of notnot2 106. This proof is notnot2ALTVD 28384 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | con3ALT 27973 | Contraposition. Alternate proof of con3 128. This proof is con3ALTVD 28385 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ssralv2 27974* |
Quantification restricted to a subclass for two quantifiers. ssralv 3364
for two quantifiers. The proof of ssralv2 27974 was automatically generated
by minimizing the automatically translated proof of ssralv2VD 28335. The
automatic translation is by the tools program
translate_{without}_overwriting.cmd
(Contributed by Alan Sare,
18-Feb-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
| ||||||||||||||||||||||||||||||

Theorem | sbc3org 27975 | sbcorg 3163 with a 3-disjuncts. This proof is sbc3orgVD 28320 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | alrim3con13v 27976* | Closed form of alrimi 1777 with 2 additional conjuncts having no occurences of the quantifying variable. This proof is 19.21a3con13vVD 28321 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | rspsbc2 27977* | rspsbc 3196 with two quantifying variables. This proof is rspsbc2VD 28324 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcoreleleq 27978* | Substitution of a set variable for another set variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 28328. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | tratrb 27979* | If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD 28330. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 3ax5 27980 | ax-5 1563 for a 3 element left-nested implication. Derived automatically from 3ax5VD 28331. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ordelordALT 27981 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4558 using the Axiom of Regularity indirectly through dford2 7522. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that because this is inferred by the Axiom of Regularity. ordelordALT 27981 is ordelordALTVD 28336 without virtual deductions and was automatically derived from ordelordALTVD 28336 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcim2g 27982 | Distribution of class substitution over a left-nested implication. Similar to sbcimg 3159. sbcim2g 27982 is sbcim2gVD 28344 without virtual deductions and was automatically derived from sbcim2gVD 28344 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcbi 27983 | Implication form of sbcbiiOLD 3174. sbcbi 27983 is sbcbiVD 28345 without virtual deductions and was automatically derived from sbcbiVD 28345 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | trsbc 27984* | Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. trsbc 27984 is trsbcVD 28346 without virtual deductions and was automatically derived from trsbcVD 28346 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | truniALT 27985* | The union of a class of transitive sets is transitive. Alternate proof of truni 4271. truniALT 27985 is truniALTVD 28347 without virtual deductions and was automatically derived from truniALTVD 28347 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | sbcssOLD 27986 | Distribute proper substitution through a subclass relation. This theorem was automatically derived from sbcssVD 28352. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem5 27987* | Lemma for onfrALT 27994. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem4 27988* | Lemma for onfrALT 27994. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem3 27989* | Lemma for onfrALT 27994. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | ggen31 27990* | gen31 28079 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem2 27991* | |||||||||||||||||||||||||||||||

Theorem | cbvexsv 27992* | A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | onfrALTlem1 27993* | |||||||||||||||||||||||||||||||

Theorem | onfrALT 27994 | The epsilon relation is foundational on the class of ordinal numbers. onfrALT 27994 is an alternate proof of onfr 4575. onfrALTVD 28360 is the Virtual Deduction proof from which onfrALT 27994 is derived. The Virtual Deduction proof mirrors the working proof of onfr 4575 which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of [TakeutiZaring] p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD 28360. This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | csbeq2g 27995 | Formula-building implication rule for class substitution. Closed form of csbeq2i 3234. csbeq2g 27995 is derived from the virtual deduction proof csbeq2gVD 28361. (Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 19.41rg 27996 | Closed form of right-to-left implication of 19.41 1896, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 28371. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | opelopab4 27997* | Ordered pair membership in a class abstraction of pairs. Compare to elopab 4417. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | 2pm13.193 27998 | pm13.193 27296 for two variables. pm13.193 27296 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 28372. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbntal 27999 | A closed form of hbn 1797. hbnt 1795 is another closed form of hbn 1797. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

Theorem | hbimpg 28000 | A closed form of hbim 1832. Derived from hbimpgVD 28373. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |