Home | Metamath
Proof Explorer Theorem List (p. 415 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ofoacom 41401 | Component-wise addition of natural numnber-yielding functions commutes. (Contributed by RP, 5-Jan-2025.) |
β’ ((π΄ β π β§ (πΉ β (Ο βm π΄) β§ πΊ β (Ο βm π΄))) β (πΉ βf +o πΊ) = (πΊ βf +o πΉ)) | ||
Theorem | naddcnff 41402 | Addition operator for Cantor normal forms is a function into Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)):(π Γ π)βΆπ) | ||
Theorem | naddcnffn 41403 | Addition operator for Cantor normal forms is a function. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)) Fn (π Γ π)) | ||
Theorem | naddcnffo 41404 | Addition of Cantor normal forms is a function onto Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ ((π β On β§ π = dom (Ο CNF π)) β ( βf +o βΎ (π Γ π)):(π Γ π)βontoβπ) | ||
Theorem | naddcnfcl 41405 | Closure law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 2-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π)) β (πΉ βf +o πΊ) β π) | ||
Theorem | naddcnfcom 41406 | Component-wise ordinal addition of Cantor normal forms commutes. (Contributed by RP, 2-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π)) β (πΉ βf +o πΊ) = (πΊ βf +o πΉ)) | ||
Theorem | naddcnfid1 41407 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ πΉ β π) β (πΉ βf +o (π Γ {β })) = πΉ) | ||
Theorem | naddcnfid2 41408 | Identity law for component-wise ordinal addition of Cantor normal forms. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ πΉ β π) β ((π Γ {β }) βf +o πΉ) = πΉ) | ||
Theorem | naddcnfass 41409 | Component-wise addition of Cantor normal forms is associative. (Contributed by RP, 3-Jan-2025.) |
β’ (((π β On β§ π = dom (Ο CNF π)) β§ (πΉ β π β§ πΊ β π β§ π» β π)) β ((πΉ βf +o πΊ) βf +o π») = (πΉ βf +o (πΊ βf +o π»))) | ||
Theorem | abeqabi 41410 | Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024.) |
β’ π΄ = {π₯ β£ π} β β’ ({π₯ β£ π} = π΄ β βπ₯(π β π)) | ||
Theorem | abpr 41411* | Condition for a class abstraction to be a pair. (Contributed by RP, 25-Aug-2024.) |
β’ ({π₯ β£ π} = {π, π} β βπ₯(π β (π₯ = π β¨ π₯ = π))) | ||
Theorem | abtp 41412* | Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024.) |
β’ ({π₯ β£ π} = {π, π, π} β βπ₯(π β (π₯ = π β¨ π₯ = π β¨ π₯ = π))) | ||
Theorem | ralopabb 41413* | Restricted universal quantification over an ordered-pair class abstraction. (Contributed by RP, 25-Sep-2024.) |
β’ π = {β¨π₯, π¦β© β£ π} & β’ (π = β¨π₯, π¦β© β (π β π)) β β’ (βπ β π π β βπ₯βπ¦(π β π)) | ||
Theorem | bropabg 41414* | Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt 27047. (Contributed by RP, 26-Sep-2024.) |
β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ π = {β¨π₯, π¦β© β£ π} β β’ (π΄π π΅ β ((π΄ β V β§ π΅ β V) β§ π)) | ||
Theorem | fpwfvss 41415 | Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024.) |
β’ πΉ:πΆβΆπ« π΅ β β’ (πΉβπ΄) β π΅ | ||
Theorem | sdomne0 41416 | A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.) |
β’ (π΅ βΊ π΄ β π΄ β β ) | ||
Theorem | sdomne0d 41417 | A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.) |
β’ (π β π΅ βΊ π΄) & β’ (π β π΅ β π) β β’ (π β π΄ β β ) | ||
Theorem | safesnsupfiss 41418 | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) β β’ (π β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅) β π΅) | ||
Theorem | safesnsupfiub 41419* | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) & β’ (π β βπ₯ β π΅ βπ¦ β πΆ π₯π π¦) β β’ (π β βπ₯ β if (π βΊ π΅, {sup(π΅, π΄, π )}, π΅)βπ¦ β πΆ π₯π π¦) | ||
Theorem | safesnsupfidom1o 41420 | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) β β’ (π β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅) βΌ 1o) | ||
Theorem | safesnsupfilb 41421* | If π΅ is a finite subset of ordered class π΄, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 3-Sep-2024.) |
β’ (π β (π = β β¨ π = 1o)) & β’ (π β π΅ β Fin) & β’ (π β π΅ β π΄) & β’ (π β π Or π΄) β β’ (π β βπ₯ β (π΅ β if(π βΊ π΅, {sup(π΅, π΄, π )}, π΅))βπ¦ β if (π βΊ π΅, {sup(π΅, π΄, π )}, π΅)π₯π π¦) | ||
Theorem | isoeq145d 41422 | Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.) |
β’ (π β πΉ = πΊ) & β’ (π β π΄ = πΆ) & β’ (π β π΅ = π·) β β’ (π β (πΉ Isom π , π (π΄, π΅) β πΊ Isom π , π (πΆ, π·))) | ||
Theorem | resisoeq45d 41423 | Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.) |
β’ (π β π΄ = πΆ) & β’ (π β π΅ = π·) β β’ (π β ((πΉ βΎ π΄) Isom π , π (π΄, π΅) β (πΉ βΎ πΆ) Isom π , π (πΆ, π·))) | ||
Theorem | negslem1 41424 | An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.) |
β’ (π΄ = π΅ β ((πΉ βΎ π΄) Isom π , β‘π (π΄, π΄) β (πΉ βΎ π΅) Isom π , β‘π (π΅, π΅))) | ||
Theorem | nvocnvb 41425* | Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024.) |
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (πΉ:π΄β1-1-ontoβπ΄ β§ βπ₯ β π΄ (πΉβ(πΉβπ₯)) = π₯)) | ||
Theorem | rp-brsslt 41426* | Binary relation form of a relation, <, which has been extended from relation π to subsets of class π. Usually, we will assume π Or π. Definition in [Alling], p. 2. Generalization of brsslt 27047. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} β β’ (π΄ < π΅ β ((π΄ β V β§ π΅ β V) β§ (π΄ β π β§ π΅ β π β§ βπ₯ β π΄ βπ¦ β π΅ π₯π π¦))) | ||
Theorem | nla0002 41427* | Extending a linear order to subsets, the empty set is less than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} & β’ (π β π΄ β V) & β’ (π β π΄ β π) β β’ (π β β < π΄) | ||
Theorem | nla0003 41428* | Extending a linear order to subsets, the empty set is greater than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} & β’ (π β π΄ β V) & β’ (π β π΄ β π) β β’ (π β π΄ < β ) | ||
Theorem | nla0001 41429* | Extending a linear order to subsets, the empty set is less than itself. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.) |
β’ < = {β¨π, πβ© β£ (π β π β§ π β π β§ βπ₯ β π βπ¦ β π π₯π π¦)} β β’ (π β β < β ) | ||
Theorem | faosnf0.11b 41430* |
π΅
is called a non-limit ordinal if it is not a limit ordinal.
(Contributed by RP, 27-Sep-2023.)
Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243. |
β’ ((Ord π΄ β§ Β¬ Lim π΄ β§ π΄ β β ) β βπ₯ β On π΄ = suc π₯) | ||
Theorem | dfno2 41431 | A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.) |
β’ No = {π β π« (On Γ {1o, 2o}) β£ (Fun π β§ dom π β On)} | ||
Theorem | onnog 41432 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β {1o, 2o}) β (π΄ Γ {π΅}) β No ) | ||
Theorem | onnobdayg 41433 | Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β On β§ π΅ β {1o, 2o}) β ( bday β(π΄ Γ {π΅})) = π΄) | ||
Theorem | bdaybndex 41434 | Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.) |
β’ ((π΄ β No β§ π΅ = ( bday βπ΄) β§ πΆ β {1o, 2o}) β (π΅ Γ {πΆ}) β No ) | ||
Theorem | bdaybndbday 41435 | Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.) |
β’ ((π΄ β No β§ π΅ = ( bday βπ΄) β§ πΆ β {1o, 2o}) β ( bday β(π΅ Γ {πΆ})) = ( bday βπ΄)) | ||
Theorem | onno 41436 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (π΄ β On β (π΄ Γ {2o}) β No ) | ||
Theorem | onnoi 41437 | Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ π΄ β On β β’ (π΄ Γ {2o}) β No | ||
Theorem | 0no 41438 | Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ β β No | ||
Theorem | 1no 41439 | Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (1o Γ {2o}) β No | ||
Theorem | 2no 41440 | Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (2o Γ {2o}) β No | ||
Theorem | 3no 41441 | Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (3o Γ {2o}) β No | ||
Theorem | 4no 41442 | Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.) |
β’ (4o Γ {2o}) β No | ||
Theorem | fnimafnex 41443 | The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.) |
β’ πΉ Fn π΅ β β’ (πΉ β (πΊβπ΄)) β V | ||
Theorem | nlimsuc 41444 | A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ (π΄ β On β Β¬ Lim suc π΄) | ||
Theorem | nlim1NEW 41445 | 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
β’ Β¬ Lim 1o | ||
Theorem | nlim2NEW 41446 | 2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.) |
β’ Β¬ Lim 2o | ||
Theorem | nlim3 41447 | 3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ Β¬ Lim 3o | ||
Theorem | nlim4 41448 | 4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.) |
β’ Β¬ Lim 4o | ||
Theorem | oa1un 41449 | Given π΄ β On, let π΄ +o 1o be defined to be the union of π΄ and {π΄}. Compare with oa1suc 8445. (Contributed by RP, 27-Sep-2023.) |
β’ (π΄ β On β (π΄ +o 1o) = (π΄ βͺ {π΄})) | ||
Theorem | oa1cl 41450 | π΄ +o 1o is in On. (Contributed by RP, 27-Sep-2023.) |
β’ (π΄ β On β (π΄ +o 1o) β On) | ||
Theorem | 0finon 41451 | 0 is a finite ordinal. See peano1 7816. (Contributed by RP, 27-Sep-2023.) |
β’ β β (On β© Fin) | ||
Theorem | 1finon 41452 | 1 is a finite ordinal. See 1onn 8554. (Contributed by RP, 27-Sep-2023.) |
β’ 1o β (On β© Fin) | ||
Theorem | 2finon 41453 | 2 is a finite ordinal. See 1onn 8554. (Contributed by RP, 27-Sep-2023.) |
β’ 2o β (On β© Fin) | ||
Theorem | 3finon 41454 | 3 is a finite ordinal. See 1onn 8554. (Contributed by RP, 27-Sep-2023.) |
β’ 3o β (On β© Fin) | ||
Theorem | 4finon 41455 | 4 is a finite ordinal. See 1onn 8554. (Contributed by RP, 27-Sep-2023.) |
β’ 4o β (On β© Fin) | ||
Theorem | finona1cl 41456 | The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.) |
β’ (π β (On β© Fin) β (π +o 1o) β (On β© Fin)) | ||
Theorem | finonex 41457 | The finite ordinals are a set. See also onprc 7703 and fiprc 8923 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.) |
β’ (On β© Fin) β V | ||
Theorem | fzunt 41458 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ (πΎ β€ π β§ π β€ π)) β ((πΎ...π) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzuntd 41459 | Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ π) β β’ (π β ((πΎ...π) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzunt1d 41460 | Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β πΏ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ πΏ) & β’ (π β πΏ β€ π) β β’ (π β ((πΎ...πΏ) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | fzuntgd 41461 | Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.) |
β’ (π β πΎ β β€) & β’ (π β πΏ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β€ π) & β’ (π β π β€ (πΏ + 1)) & β’ (π β πΏ β€ π) β β’ (π β ((πΎ...πΏ) βͺ (π...π)) = (πΎ...π)) | ||
Theorem | ifpan123g 41462 | Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.) |
β’ ((if-(π, π, π) β§ if-(π, π, π)) β (((Β¬ π β¨ π) β§ (π β¨ π)) β§ ((Β¬ π β¨ π) β§ (π β¨ π)))) | ||
Theorem | ifpan23 41463 | Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.) |
β’ ((if-(π, π, π) β§ if-(π, π, π)) β if-(π, (π β§ π), (π β§ π))) | ||
Theorem | ifpdfor2 41464 | Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β¨ π) β if-(π, π, π)) | ||
Theorem | ifporcor 41465 | Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.) |
β’ (if-(π, π, π) β if-(π, π, π)) | ||
Theorem | ifpdfan2 41466 | Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
β’ ((π β§ π) β if-(π, π, π)) | ||
Theorem | ifpancor 41467 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, π, π) β if-(π, π, π)) | ||
Theorem | ifpdfor 41468 | Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β¨ π) β if-(π, β€, π)) | ||
Theorem | ifpdfan 41469 | Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β§ π) β if-(π, π, β₯)) | ||
Theorem | ifpbi2 41470 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
β’ ((π β π) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpbi3 41471 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
β’ ((π β π) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpim1 41472 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β π) β if-(Β¬ π, β€, π)) | ||
Theorem | ifpnot 41473 | Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ (Β¬ π β if-(π, β₯, β€)) | ||
Theorem | ifpid2 41474 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ (π β if-(π, β€, β₯)) | ||
Theorem | ifpim2 41475 | Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β π) β if-(π, β€, Β¬ π)) | ||
Theorem | ifpbi23 41476 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
β’ (((π β π) β§ (π β π)) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpbiidcor 41477 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
β’ if-(π, π, Β¬ π) | ||
Theorem | ifpbicor 41478 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, π, Β¬ π) β if-(π, π, Β¬ π)) | ||
Theorem | ifpxorcor 41479 | Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, Β¬ π, π) β if-(π, Β¬ π, π)) | ||
Theorem | ifpbi1 41480 | Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.) |
β’ ((π β π) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpnot23 41481 | Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
β’ (Β¬ if-(π, π, π) β if-(π, Β¬ π, Β¬ π)) | ||
Theorem | ifpnotnotb 41482 | Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.) |
β’ (if-(π, Β¬ π, Β¬ π) β Β¬ if-(π, π, π)) | ||
Theorem | ifpnorcor 41483 | Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, Β¬ π, Β¬ π) β if-(π, Β¬ π, Β¬ π)) | ||
Theorem | ifpnancor 41484 | Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.) |
β’ (if-(π, Β¬ π, Β¬ π) β if-(π, Β¬ π, Β¬ π)) | ||
Theorem | ifpnot23b 41485 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
β’ (Β¬ if-(π, Β¬ π, π) β if-(π, π, Β¬ π)) | ||
Theorem | ifpbiidcor2 41486 | Restatement of biid 261. (Contributed by RP, 25-Apr-2020.) |
β’ Β¬ if-(π, Β¬ π, π) | ||
Theorem | ifpnot23c 41487 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
β’ (Β¬ if-(π, π, Β¬ π) β if-(π, Β¬ π, π)) | ||
Theorem | ifpnot23d 41488 | Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.) |
β’ (Β¬ if-(π, Β¬ π, Β¬ π) β if-(π, π, π)) | ||
Theorem | ifpdfnan 41489 | Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π βΌ π) β if-(π, Β¬ π, β€)) | ||
Theorem | ifpdfxor 41490 | Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β» π) β if-(π, Β¬ π, π)) | ||
Theorem | ifpbi12 41491 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
β’ (((π β π) β§ (π β π)) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpbi13 41492 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
β’ (((π β π) β§ (π β π)) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpbi123 41493 | Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.) |
β’ (((π β π) β§ (π β π) β§ (π β π)) β (if-(π, π, π) β if-(π, π, π))) | ||
Theorem | ifpidg 41494 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β if-(π, π, π)) β ((((π β§ π) β π) β§ ((π β§ π) β π)) β§ ((π β (π β¨ π)) β§ (π β (π β¨ π))))) | ||
Theorem | ifpid3g 41495 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β if-(π, π, π)) β (((π β§ π) β π) β§ ((π β§ π) β π))) | ||
Theorem | ifpid2g 41496 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β if-(π, π, π)) β ((π β (π β¨ π)) β§ (π β (π β¨ π)))) | ||
Theorem | ifpid1g 41497 | Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.) |
β’ ((π β if-(π, π, π)) β ((π β π) β§ (π β π))) | ||
Theorem | ifpim23g 41498 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
β’ (((π β π) β if-(π, π, Β¬ π)) β (((π β§ π) β π) β§ (π β (π β¨ π)))) | ||
Theorem | ifpim3 41499 | Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
β’ ((π β π) β if-(π, π, Β¬ π)) | ||
Theorem | ifpnim1 41500 | Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.) |
β’ (Β¬ (π β π) β if-(π, Β¬ π, π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |