Home | Metamath
Proof Explorer Theorem List (p. 426 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description | ||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||
Theorem | addcomgi 42501 | Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||||||||
โข (๐ด + ๐ต) = (๐ต + ๐ด) | ||||||||||||||||||||||||||||||||
Syntax | cplusr 42502 | Introduce the operation of vector addition. | ||||||||||||||||||||||||||||||
class +๐ | ||||||||||||||||||||||||||||||||
Syntax | cminusr 42503 | Introduce the operation of vector subtraction. | ||||||||||||||||||||||||||||||
class -๐ | ||||||||||||||||||||||||||||||||
Syntax | ctimesr 42504 | Introduce the operation of scalar multiplication. | ||||||||||||||||||||||||||||||
class .๐ฃ | ||||||||||||||||||||||||||||||||
Syntax | cptdfc 42505 | PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems. | ||||||||||||||||||||||||||||||
class PtDf(๐ด, ๐ต) | ||||||||||||||||||||||||||||||||
Syntax | crr3c 42506 | RR3 is a class. | ||||||||||||||||||||||||||||||
class RR3 | ||||||||||||||||||||||||||||||||
Syntax | cline3 42507 | line3 is a class. | ||||||||||||||||||||||||||||||
class line3 | ||||||||||||||||||||||||||||||||
Definition | df-addr 42508* | Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข +๐ = (๐ฅ โ V, ๐ฆ โ V โฆ (๐ฃ โ โ โฆ ((๐ฅโ๐ฃ) + (๐ฆโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Definition | df-subr 42509* | Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข -๐ = (๐ฅ โ V, ๐ฆ โ V โฆ (๐ฃ โ โ โฆ ((๐ฅโ๐ฃ) โ (๐ฆโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Definition | df-mulv 42510* | Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข .๐ฃ = (๐ฅ โ V, ๐ฆ โ V โฆ (๐ฃ โ โ โฆ (๐ฅ ยท (๐ฆโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Theorem | addrval 42511* | Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด+๐๐ต) = (๐ฃ โ โ โฆ ((๐ดโ๐ฃ) + (๐ตโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Theorem | subrval 42512* | Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด-๐๐ต) = (๐ฃ โ โ โฆ ((๐ดโ๐ฃ) โ (๐ตโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Theorem | mulvval 42513* | Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด.๐ฃ๐ต) = (๐ฃ โ โ โฆ (๐ด ยท (๐ตโ๐ฃ)))) | ||||||||||||||||||||||||||||||||
Theorem | addrfv 42514 | Vector addition at a value. The operation takes each vector ๐ด and ๐ต and forms a new vector whose values are the sum of each of the values of ๐ด and ๐ต. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ธ โง ๐ต โ ๐ท โง ๐ถ โ โ) โ ((๐ด+๐๐ต)โ๐ถ) = ((๐ดโ๐ถ) + (๐ตโ๐ถ))) | ||||||||||||||||||||||||||||||||
Theorem | subrfv 42515 | Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ธ โง ๐ต โ ๐ท โง ๐ถ โ โ) โ ((๐ด-๐๐ต)โ๐ถ) = ((๐ดโ๐ถ) โ (๐ตโ๐ถ))) | ||||||||||||||||||||||||||||||||
Theorem | mulvfv 42516 | Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ธ โง ๐ต โ ๐ท โง ๐ถ โ โ) โ ((๐ด.๐ฃ๐ต)โ๐ถ) = (๐ด ยท (๐ตโ๐ถ))) | ||||||||||||||||||||||||||||||||
Theorem | addrfn 42517 | Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด+๐๐ต) Fn โ) | ||||||||||||||||||||||||||||||||
Theorem | subrfn 42518 | Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด-๐๐ต) Fn โ) | ||||||||||||||||||||||||||||||||
Theorem | mulvfn 42519 | Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด.๐ฃ๐ต) Fn โ) | ||||||||||||||||||||||||||||||||
Theorem | addrcom 42520 | Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.) | ||||||||||||||||||||||||||||||
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ท) โ (๐ด+๐๐ต) = (๐ต+๐๐ด)) | ||||||||||||||||||||||||||||||||
Definition | df-ptdf 42521* | Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
โข PtDf(๐ด, ๐ต) = (๐ฅ โ โ โฆ (((๐ฅ.๐ฃ(๐ต-๐๐ด)) +๐ฃ ๐ด) โ {1, 2, 3})) | ||||||||||||||||||||||||||||||||
Definition | df-rr3 42522 | Define the set of all points RR3. We define each point ๐ด as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
โข RR3 = (โ โm {1, 2, 3}) | ||||||||||||||||||||||||||||||||
Definition | df-line3 42523* | Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.) | ||||||||||||||||||||||||||||||
โข line3 = {๐ฅ โ ๐ซ RR3 โฃ (2o โผ ๐ฅ โง โ๐ฆ โ ๐ฅ โ๐ง โ ๐ฅ (๐ง โ ๐ฆ โ ran PtDf(๐ฆ, ๐ง) = ๐ฅ))} | ||||||||||||||||||||||||||||||||
We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019). Alan's first contribution to Metamath was a shorter proof for tfrlem8 8298 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof 8298. His virtual deduction method is explained in the comment for wvd1 42616. Below are some excerpts from his first emails to NM in 2007: ...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the Metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me.... ...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way.... ...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof.... | ||||||||||||||||||||||||||||||||
Theorem | idiALT 42524 | Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ๐ โ โข ๐ | ||||||||||||||||||||||||||||||||
Theorem | exbir 42525 | Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 42900. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
โข (((๐ โง ๐) โ (๐ โ ๐)) โ (๐ โ (๐ โ (๐ โ ๐)))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicom 42526 | Version of 3impexp 1359 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
โข (((๐ โง ๐ โง ๐) โ (๐ โ ๐)) โ (๐ โ (๐ โ (๐ โ (๐ โ ๐))))) | ||||||||||||||||||||||||||||||||
Theorem | 3impexpbicomi 42527 | Inference associated with 3impexpbicom 42526. Derived automatically from 3impexpbicomiVD 42905. (Contributed by Alan Sare, 31-Dec-2011.) | ||||||||||||||||||||||||||||||
โข ((๐ โง ๐ โง ๐) โ (๐ โ ๐)) โ โข (๐ โ (๐ โ (๐ โ (๐ โ ๐)))) | ||||||||||||||||||||||||||||||||
Theorem | bi1imp 42528 | Importation inference similar to imp 408, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ ๐)) โ โข ((๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi2imp 42529 | Importation inference similar to imp 408, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ ๐)) โ โข ((๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi3impb 42530 | Similar to 3impb 1116 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข ((๐ โง (๐ โง ๐)) โ ๐) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi3impa 42531 | Similar to 3impa 1111 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (((๐ โง ๐) โง ๐) โ ๐) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi23impib 42532 | 3impib 1117 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ ((๐ โง ๐) โ ๐)) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi13impib 42533 | 3impib 1117 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ ((๐ โง ๐) โ ๐)) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi123impib 42534 | 3impib 1117 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ ((๐ โง ๐) โ ๐)) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi13impia 42535 | 3impia 1118 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข ((๐ โง ๐) โ (๐ โ ๐)) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi123impia 42536 | 3impia 1118 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข ((๐ โง ๐) โ (๐ โ ๐)) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi33imp12 42537 | 3imp 1112 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp13 42538 | 3imp 1112 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp23 42539 | 3imp 1112 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi13imp2 42540 | Similar to 3imp 1112 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi12imp3 42541 | Similar to 3imp 1112 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi23imp1 42542 | Similar to 3imp 1112 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | bi123imp0 42543 | Similar to 3imp 1112 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข ((๐ โง ๐ โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 4animp1 42544 | A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
โข ((๐ โง ๐ โง ๐) โ (๐ โ ๐)) โ โข ((((๐ โง ๐) โง ๐) โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 4an31 42545 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
โข ((((๐ โง ๐) โง ๐) โง ๐) โ ๐) โ โข ((((๐ โง ๐) โง ๐) โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | 4an4132 42546 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) | ||||||||||||||||||||||||||||||
โข ((((๐ โง ๐) โง ๐) โง ๐) โ ๐) โ โข ((((๐ โง ๐) โง ๐) โง ๐) โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | expcomdg 42547 | Biconditional form of expcomd 418. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ ((๐ โง ๐) โ ๐)) โ (๐ โ (๐ โ (๐ โ ๐)))) | ||||||||||||||||||||||||||||||||
Theorem | iidn3 42548 | idn3 42662 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | ee222 42549 | e222 42683 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | ee3bir 42550 | Right-biconditional form of e3 42784 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ ๐) โ โข (๐ โ (๐ โ (๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | ee13 42551 | e13 42795 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐) & โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ ๐)) โ โข (๐ โ (๐ โ (๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | ee121 42552 | e121 42703 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ ๐) & โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | ee122 42553 | e122 42700 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ ๐) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | ee333 42554 | e333 42780 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ (๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | ee323 42555 | e323 42813 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ (๐ โ (๐ โ ๐))) & โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ (๐ โ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | 3ornot23 42556 | If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 42894. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((ยฌ ๐ โง ยฌ ๐) โ ((๐ โจ ๐ โจ ๐) โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | orbi1r 42557 | orbi1 917 with order of disjuncts reversed. Derived from orbi1rVD 42895. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ ๐) โ ((๐ โจ ๐) โ (๐ โจ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | 3orbi123 42558 | pm4.39 976 with a 3-conjunct antecedent. This proof is 3orbi123VD 42897 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (((๐ โ ๐) โง (๐ โ ๐) โง (๐ โ ๐)) โ ((๐ โจ ๐ โจ ๐) โ (๐ โจ ๐ โจ ๐))) | ||||||||||||||||||||||||||||||||
Theorem | syl5imp 42559 | Closed form of syl5 34. Derived automatically from syl5impVD 42910. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ (๐ โ ๐)) โ ((๐ โ ๐) โ (๐ โ (๐ โ ๐)))) | ||||||||||||||||||||||||||||||||
Theorem | impexpd 42560 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. 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 42561 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. 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 | impexpdcom 42562 |
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. 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 42563 |
Non-virtual deduction form of e1111 42722. (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 L. 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 42564 |
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 L. 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 42565 |
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 L. 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 42566 |
Non-virtual deduction form of e233 42812. (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 L. 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 | imbi13 42567 | Join three logical equivalences to form equivalence of implications. imbi13 42567 is imbi13VD 42921 without virtual deductions and was automatically derived from imbi13VD 42921 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 42568 |
Non-virtual deduction form of e33 42781. (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 L. 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 42569 | Biconditional contraposition variation. This proof is con5VD 42947 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ ยฌ ๐) โ (ยฌ ๐ โ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | con5i 42570 | Inference form of con5 42569. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ ยฌ ๐) โ โข (ยฌ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | exlimexi 42571 | 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 42572* | Equivalence for substitution. Alternate proof of sb5 2269. This proof is sb5ALTVD 42960 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ([๐ฆ / ๐ฅ]๐ โ โ๐ฅ(๐ฅ = ๐ฆ โง ๐)) | ||||||||||||||||||||||||||||||||
Theorem | eexinst01 42573 | exinst01 42672 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข โ๐ฅ๐ & โข (๐ โ (๐ โ ๐)) & โข (๐ โ โ๐ฅ๐) & โข (๐ โ โ๐ฅ๐) โ โข (๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | eexinst11 42574 | exinst11 42673 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ โ๐ฅ๐) & โข (๐ โ (๐ โ ๐)) & โข (๐ โ โ๐ฅ๐) & โข (๐ โ โ๐ฅ๐) โ โข (๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | vk15.4j 42575 | 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 42575 is vk15.4jVD 42961 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ยฌ (โ๐ฅ ยฌ ๐ โง โ๐ฅ(๐ โง ยฌ ๐)) & โข (โ๐ฅ๐ โ ยฌ โ๐ฅ(๐ โง ๐)) & โข ยฌ โ๐ฅ(๐ โ ๐) โ โข (ยฌ โ๐ฅ ยฌ ๐ โ ยฌ โ๐ฅ๐) | ||||||||||||||||||||||||||||||||
Theorem | notnotrALT 42576 | Converse of double negation. Alternate proof of notnotr 130. This proof is notnotrALTVD 42962 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (ยฌ ยฌ ๐ โ ๐) | ||||||||||||||||||||||||||||||||
Theorem | con3ALT2 42577 | Contraposition. Alternate proof of con3 153. This proof is con3ALTVD 42963 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ ๐) โ (ยฌ ๐ โ ยฌ ๐)) | ||||||||||||||||||||||||||||||||
Theorem | ssralv2 42578* | Quantification restricted to a subclass for two quantifiers. ssralv 4009 for two quantifiers. The proof of ssralv2 42578 was automatically generated by minimizing the automatically translated proof of ssralv2VD 42913. 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 | sbc3or 42579 | sbcor 3791 with a 3-disjuncts. This proof is sbc3orgVD 42898 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ([๐ด / ๐ฅ](๐ โจ ๐ โจ ๐) โ ([๐ด / ๐ฅ]๐ โจ [๐ด / ๐ฅ]๐ โจ [๐ด / ๐ฅ]๐)) | ||||||||||||||||||||||||||||||||
Theorem | alrim3con13v 42580* | Closed form of alrimi 2207 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 42899 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ โ๐ฅ๐) โ ((๐ โง ๐ โง ๐) โ โ๐ฅ(๐ โง ๐ โง ๐))) | ||||||||||||||||||||||||||||||||
Theorem | rspsbc2 42581* | rspsbc 3834 with two quantifying variables. This proof is rspsbc2VD 42902 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ด โ ๐ต โ (๐ถ โ ๐ท โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ท ๐ โ [๐ถ / ๐ฆ][๐ด / ๐ฅ]๐))) | ||||||||||||||||||||||||||||||||
Theorem | sbcoreleleq 42582* | Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 42906. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ด โ ๐ โ ([๐ด / ๐ฆ](๐ฅ โ ๐ฆ โจ ๐ฆ โ ๐ฅ โจ ๐ฅ = ๐ฆ) โ (๐ฅ โ ๐ด โจ ๐ด โ ๐ฅ โจ ๐ฅ = ๐ด))) | ||||||||||||||||||||||||||||||||
Theorem | tratrb 42583* | 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 42908. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((Tr ๐ด โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด (๐ฅ โ ๐ฆ โจ ๐ฆ โ ๐ฅ โจ ๐ฅ = ๐ฆ) โง ๐ต โ ๐ด) โ Tr ๐ต) | ||||||||||||||||||||||||||||||||
Theorem | ordelordALT 42584 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6336 using the Axiom of Regularity indirectly through dford2 9490. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that E Fr ๐ด because this is inferred by the Axiom of Regularity. ordelordALT 42584 is ordelordALTVD 42914 without virtual deductions and was automatically derived from ordelordALTVD 42914 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.) | ||||||||||||||||||||||||||||||
โข ((Ord ๐ด โง ๐ต โ ๐ด) โ Ord ๐ต) | ||||||||||||||||||||||||||||||||
Theorem | sbcim2g 42585 | Distribution of class substitution over a left-nested implication. Similar to sbcimg 3789. sbcim2g 42585 is sbcim2gVD 42922 without virtual deductions and was automatically derived from sbcim2gVD 42922 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 42586 | Implication form of sbcbii 3798. sbcbi 42586 is sbcbiVD 42923 without virtual deductions and was automatically derived from sbcbiVD 42923 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 42587* | Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 42587 is trsbcVD 42924 without virtual deductions and was automatically derived from trsbcVD 42924 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.) | ||||||||||||||||||||||||||||||
โข (๐ด โ ๐ โ ([๐ด / ๐ฅ]Tr ๐ฅ โ Tr ๐ด)) | ||||||||||||||||||||||||||||||||
Theorem | truniALT 42588* | The union of a class of transitive sets is transitive. Alternate proof of truni 5237. truniALT 42588 is truniALTVD 42925 without virtual deductions and was automatically derived from truniALTVD 42925 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.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅ โ ๐ด Tr ๐ฅ โ Tr โช ๐ด) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem5 42589* | Lemma for onfrALT 42596. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ([(๐ โฉ ๐ฅ) / ๐]((๐ โ (๐ โฉ ๐ฅ) โง ๐ โ โ ) โ โ๐ฆ โ ๐ (๐ โฉ ๐ฆ) = โ ) โ (((๐ โฉ ๐ฅ) โ (๐ โฉ ๐ฅ) โง (๐ โฉ ๐ฅ) โ โ ) โ โ๐ฆ โ (๐ โฉ ๐ฅ)((๐ โฉ ๐ฅ) โฉ ๐ฆ) = โ )) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem4 42590* | Lemma for onfrALT 42596. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ([๐ฆ / ๐ฅ](๐ฅ โ ๐ โง (๐ โฉ ๐ฅ) = โ ) โ (๐ฆ โ ๐ โง (๐ โฉ ๐ฆ) = โ )) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem3 42591* | Lemma for onfrALT 42596. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ On โง ๐ โ โ ) โ ((๐ฅ โ ๐ โง ยฌ (๐ โฉ ๐ฅ) = โ ) โ โ๐ฆ โ (๐ โฉ ๐ฅ)((๐ โฉ ๐ฅ) โฉ ๐ฆ) = โ )) | ||||||||||||||||||||||||||||||||
Theorem | ggen31 42592* | gen31 42668 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (๐ โ (๐ โ (๐ โ ๐))) โ โข (๐ โ (๐ โ (๐ โ โ๐ฅ๐))) | ||||||||||||||||||||||||||||||||
Theorem | onfrALTlem2 42593* | Lemma for onfrALT 42596. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ On โง ๐ โ โ ) โ ((๐ฅ โ ๐ โง ยฌ (๐ โฉ ๐ฅ) = โ ) โ โ๐ฆ โ ๐ (๐ โฉ ๐ฆ) = โ )) | ||||||||||||||||||||||||||||||||
Theorem | cbvexsv 42594* | 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 42595* | Lemma for onfrALT 42596. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข ((๐ โ On โง ๐ โ โ ) โ ((๐ฅ โ ๐ โง (๐ โฉ ๐ฅ) = โ ) โ โ๐ฆ โ ๐ (๐ โฉ ๐ฆ) = โ )) | ||||||||||||||||||||||||||||||||
Theorem | onfrALT 42596 | The membership relation is foundational on the class of ordinal numbers. onfrALT 42596 is an alternate proof of onfr 6353. onfrALTVD 42938 is the Virtual Deduction proof from which onfrALT 42596 is derived. The Virtual Deduction proof mirrors the working proof of onfr 6353 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 42938. 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.) | ||||||||||||||||||||||||||||||
โข E Fr On | ||||||||||||||||||||||||||||||||
Theorem | 19.41rg 42597 | Closed form of right-to-left implication of 19.41 2229, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 42949. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅ(๐ โ โ๐ฅ๐) โ ((โ๐ฅ๐ โง ๐) โ โ๐ฅ(๐ โง ๐))) | ||||||||||||||||||||||||||||||||
Theorem | opelopab4 42598* | Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab 5482. (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 42599 | pm13.193 42456 for two variables. pm13.193 42456 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 42950. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โง [๐ข / ๐ฅ][๐ฃ / ๐ฆ]๐) โ ((๐ฅ = ๐ข โง ๐ฆ = ๐ฃ) โง ๐)) | ||||||||||||||||||||||||||||||||
Theorem | hbntal 42600 | A closed form of hbn 2293. hbnt 2292 is another closed form of hbn 2293. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||||||||
โข (โ๐ฅ(๐ โ โ๐ฅ๐) โ โ๐ฅ(ยฌ ๐ โ โ๐ฅ ยฌ ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |