Home | Higher-Order Logic Explorer Theorem List (p. 1 of 3) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > HOLE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | tv 1 | A var is a term. |
term | ||
Syntax | ht 2 | The type of all functions from type to type . |
type | ||
Syntax | hb 3 | The type of booleans (true and false). |
type | ||
Syntax | hi 4 | The type of individuals. |
type | ||
Syntax | kc 5 | A combination (function application). |
term | ||
Syntax | kl 6 | A lambda abstraction. |
term | ||
Syntax | ke 7 | The equality term. |
term | ||
Syntax | kt 8 | Truth term. |
term | ||
Syntax | kbr 9 | Infix operator. |
term | ||
Syntax | kct 10 | Context operator. |
term | ||
Syntax | wffMMJ2 11 | Internal axiom for mmj2 use. |
wff | ||
Syntax | wffMMJ2t 12 | Internal axiom for mmj2 use. |
wff | ||
Theorem | idi 13 | The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.) |
Theorem | idt 14 | The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.) |
Axiom | ax-syl 15 | Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | syl 16 | Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-jca 17 | Join common antecedents. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | jca 18 | Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | syl2anc 19 | Syllogism inference. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-simpl 20 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-simpr 21 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | simpl 22 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | simpr 23 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-id 24 | The identity inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | id 25 | The identity inference. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-trud 26 | Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | trud 27 | Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | a1i 28 | Change an empty context into any context. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-cb1 29 |
A context has type boolean.
This and the next few axioms are not strictly necessary, and are conservative on any theorem for which every variable has a specified type, but by adding this axiom we can save some typehood hypotheses in many theorems. The easy way to see that this axiom is conservative is to note that every axiom and inference rule that constructs a theorem of the form where and are type variables, also ensures that and . Thus it is impossible to prove any theorem unless both and had been previously derived, so it is conservative to deduce from . The same remark applies to the construction of the theorem - there is only one rule that creates a formula of this type, namely wct 48, and it requires that and be previously established, so it is safe to reverse the process in wctl 33 and wctr 34. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-cb2 30 | A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-wctl 31 | Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) Prefer wctl 33. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-wctr 32 | Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) Prefer wctr 34. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | wctl 33 | Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | wctr 34 | Reverse closure for the type of a context. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | mpdan 35 | Modus ponens deduction. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | syldan 36 | Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | simpld 37 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | simprd 38 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | trul 39 | Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-weq 40 | The equality function has type , i.e. it is polymorphic over all types, but the left and right type must agree. (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | weq 41 | The equality function has type , i.e. it is polymorphic over all types, but the left and right type must agree. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-refl 42 | Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | wtru 43 | Truth type. (Contributed by Mario Carneiro, 10-Oct-2014.) |
Theorem | tru 44 | Tautology is provable. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-eqmp 45 | Modus ponens for equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-ded 46 | Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-wct 47 | The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.) |
Theorem | wct 48 | The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-wc 49 | The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.) |
Theorem | wc 50 | The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-ceq 51 | Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqcomx 52 | Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | mpbirx 53 | Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | ancoms 54 | Swap the two elements of a context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | adantr 55 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | adantl 56 | Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | ct1 57 | Introduce a right conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.) |
Theorem | ct2 58 | Introduce a left conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.) |
Theorem | sylan 59 | Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | an32s 60 | Commutation identity for context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | anasss 61 | Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | anassrs 62 | Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-wv 63 | The type of a typed variable. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | wv 64 | The type of a typed variable. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-wl 65 | The type of a lambda abstraction. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | wl 66 | The type of a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-beta 67 | Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-distrc 68 | Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-leq 69* | Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-distrl 70* | Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-wov 71 | Type of an infix operator. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | wov 72 | Type of an infix operator. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Definition | df-ov 73 | Infix operator. This is a simple metamath way of cleaning up the syntax of all these infix operators to make them a bit more readable than the curried representation. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | dfov1 74 | Forward direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | dfov2 75 | Reverse direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | weqi 76 | Type of an equality. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Axiom | ax-eqtypi 77 | Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqtypi 78 | Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqcomi 79 | Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Axiom | ax-eqtypri 80 | Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (New usage is discouraged.) (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqtypri 81 | Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | mpbi 82 | Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqid 83 | Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | ded 84 | Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | dedi 85 | Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | eqtru 86 | If a statement is provable, then it is equivalent to truth. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | mpbir 87 | Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | ceq12 88 | Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | ceq1 89 | Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | ceq2 90 | Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | leq 91* | Equality theorem for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | beta 92 | Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | distrc 93 | Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | distrl 94* | Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.) |
Theorem | eqtri 95 | Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | 3eqtr4i 96 | Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | 3eqtr3i 97 | Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | oveq123 98 | Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | oveq1 99 | Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.) |
Theorem | oveq12 100 | Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |