P. 1 of Theorem List - Higher-Order Logic Explorer

Theorem List for Higher-Order Logic Explorer - 1-100   *Has distinct variable group(s)

Type	Label	Description
Statement
0.1  Foundations
Syntax	tv 1	A var is a term.
term x:α
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 (FT)
Syntax	kl 6	A lambda abstraction.
term λx:α T
Syntax	ke 7	The equality term.
term =
Syntax	kt 8	Truth term.
term ⊤
Syntax	kbr 9	Infix operator.
term [AFB]
Syntax	kct 10	Context operator.
term (A, B)
Syntax	wffMMJ2 11	Internal axiom for mmj2 use.
wff A⊧B
Syntax	wffMMJ2t 12	Internal axiom for mmj2 use.
wff A:α
Theorem	idi 13	The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ R⊧A    ⇒   ⊢ R⊧A
Theorem	idt 14	The identity inference. (Contributed by Mario Carneiro, 9-Oct-2014.)
⊢ A:α    ⇒   ⊢ A:α
Axiom	ax-syl 15	Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ S⊧T    ⇒   ⊢ R⊧T
Theorem	syl 16	Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ S⊧T    ⇒   ⊢ R⊧T
Axiom	ax-jca 17	Join common antecedents. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ R⊧T    ⇒   ⊢ R⊧(S, T)
Theorem	jca 18	Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ R⊧T    ⇒   ⊢ R⊧(S, T)
Theorem	syl2anc 19	Syllogism inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R⊧S    &   ⊢ R⊧T    &   ⊢ (S, T)⊧A    ⇒   ⊢ R⊧A
Axiom	ax-simpl 20	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R:∗    &   ⊢ S:∗    ⇒   ⊢ (R, S)⊧R
Axiom	ax-simpr 21	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R:∗    &   ⊢ S:∗    ⇒   ⊢ (R, S)⊧S
Theorem	simpl 22	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R:∗    &   ⊢ S:∗    ⇒   ⊢ (R, S)⊧R
Theorem	simpr 23	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R:∗    &   ⊢ S:∗    ⇒   ⊢ (R, S)⊧S
Axiom	ax-id 24	The identity inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R:∗    ⇒   ⊢ R⊧R
Theorem	id 25	The identity inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R:∗    ⇒   ⊢ R⊧R
Axiom	ax-trud 26	Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R:∗    ⇒   ⊢ R⊧⊤
Theorem	trud 27	Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R:∗    ⇒   ⊢ R⊧⊤
Theorem	a1i 28	Change an empty context into any context. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R:∗    &   ⊢ ⊤⊧A    ⇒   ⊢ R⊧A
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 R⊧A where R and A are type variables, also ensures that R:∗ and A:∗. Thus it is impossible to prove any theorem ⊢ R⊧A unless both ⊢ R:∗ and ⊢ A:∗ had been previously derived, so it is conservative to deduce ⊢ R:∗ from ⊢ R⊧A. The same remark applies to the construction of the theorem (A, B):∗- there is only one rule that creates a formula of this type, namely wct 48, and it requires that A:∗ and B:∗ be previously established, so it is safe to reverse the process in wctl 33 and wctr 34. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧A    ⇒   ⊢ R:∗
Axiom	ax-cb2 30	A theorem has type boolean. (This axiom is unnecessary; see ax-cb1 29.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧A    ⇒   ⊢ A:∗
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.)
⊢ (S, T):∗    ⇒   ⊢ S:∗
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.)
⊢ (S, T):∗    ⇒   ⊢ T:∗
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.)
⊢ (S, T):∗    ⇒   ⊢ S:∗
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.)
⊢ (S, T):∗    ⇒   ⊢ T:∗
Theorem	mpdan 35	Modus ponens deduction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ (R, S)⊧T    ⇒   ⊢ R⊧T
Theorem	syldan 36	Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ (R, S)⊧T    &   ⊢ (R, T)⊧A    ⇒   ⊢ (R, S)⊧A
Theorem	simpld 37	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧(S, T)    ⇒   ⊢ R⊧S
Theorem	simprd 38	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧(S, T)    ⇒   ⊢ R⊧T
Theorem	trul 39	Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ (⊤, R)⊧S    ⇒   ⊢ R⊧S
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.)
⊢ A:α    ⇒   ⊢ ⊤⊧(( = A)A)
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.)
⊢ R⊧A    &   ⊢ R⊧(( = A)B)    ⇒   ⊢ R⊧B
Axiom	ax-ded 46	Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ (R, S)⊧T    &   ⊢ (R, T)⊧S    ⇒   ⊢ R⊧(( = S)T)
Axiom	ax-wct 47	The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.)
⊢ S:∗    &   ⊢ T:∗    ⇒   ⊢ (S, T):∗
Theorem	wct 48	The type of a context. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ S:∗    &   ⊢ T:∗    ⇒   ⊢ (S, T):∗
Axiom	ax-wc 49	The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.) (New usage is discouraged.)
⊢ F:(α → β)    &   ⊢ T:α    ⇒   ⊢ (FT):β
Theorem	wc 50	The type of a combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → β)    &   ⊢ T:α    ⇒   ⊢ (FT):β
Axiom	ax-ceq 51	Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → β)    &   ⊢ T:(α → β)    &   ⊢ A:α    &   ⊢ B:α    ⇒   ⊢ ((( = F)T), (( = A)B))⊧(( = (FA))(TB))
Theorem	eqcomx 52	Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ A:α    &   ⊢ B:α    &   ⊢ R⊧(( = A)B)    ⇒   ⊢ R⊧(( = B)A)
Theorem	mpbirx 53	Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ B:∗    &   ⊢ R⊧A    &   ⊢ R⊧(( = B)A)    ⇒   ⊢ R⊧B
Theorem	ancoms 54	Swap the two elements of a context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ (R, S)⊧T    ⇒   ⊢ (S, R)⊧T
Theorem	adantr 55	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧T    &   ⊢ S:∗    ⇒   ⊢ (R, S)⊧T
Theorem	adantl 56	Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧T    &   ⊢ S:∗    ⇒   ⊢ (S, R)⊧T
Theorem	ct1 57	Introduce a right conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.)
⊢ R⊧S    &   ⊢ T:∗    ⇒   ⊢ (R, T)⊧(S, T)
Theorem	ct2 58	Introduce a left conjunct. (Contributed by Mario Carneiro, 30-Sep-2023.)
⊢ R⊧S    &   ⊢ T:∗    ⇒   ⊢ (T, R)⊧(T, S)
Theorem	sylan 59	Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧S    &   ⊢ (S, T)⊧A    ⇒   ⊢ (R, T)⊧A
Theorem	an32s 60	Commutation identity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ((R, S), T)⊧A    ⇒   ⊢ ((R, T), S)⊧A
Theorem	anasss 61	Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ ((R, S), T)⊧A    ⇒   ⊢ (R, (S, T))⊧A
Theorem	anassrs 62	Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ (R, (S, T))⊧A    ⇒   ⊢ ((R, S), T)⊧A
Axiom	ax-wv 63	The type of a typed variable. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ x:α:α
Theorem	wv 64	The type of a typed variable. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ x:α:α
Axiom	ax-wl 65	The type of a lambda abstraction. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ T:β    ⇒   ⊢ λx:α T:(α → β)
Theorem	wl 66	The type of a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ T:β    ⇒   ⊢ λx:α T:(α → β)
Axiom	ax-beta 67	Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    ⇒   ⊢ ⊤⊧(( = (λx:α Ax:α))A)
Axiom	ax-distrc 68	Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ B:α    &   ⊢ F:(β → γ)    ⇒   ⊢ ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
Axiom	ax-leq 69*	Equality theorem for abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ B:β    &   ⊢ R⊧(( = A)B)    ⇒   ⊢ R⊧(( = λx:α A)λx:α B)
Axiom	ax-distrl 70*	Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ B:α    ⇒   ⊢ ⊤⊧(( = (λx:α λy:β AB))λy:β (λx:α AB))
Axiom	ax-wov 71	Type of an infix operator. (New usage is discouraged.) (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    ⇒   ⊢ [AFB]:γ
Theorem	wov 72	Type of an infix operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    ⇒   ⊢ [AFB]:γ
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.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    ⇒   ⊢ ⊤⊧(( = [AFB])((FA)B))
Theorem	dfov1 74	Forward direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → (β → ∗))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[AFB]    ⇒   ⊢ R⊧((FA)B)
Theorem	dfov2 75	Reverse direction of df-ov 73. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(α → (β → ∗))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧((FA)B)    ⇒   ⊢ R⊧[AFB]
Theorem	weqi 76	Type of an equality. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:α    &   ⊢ B:α    ⇒   ⊢ [A = B]:∗
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.)
⊢ A:α    &   ⊢ R⊧[A = B]    ⇒   ⊢ B:α
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.)
⊢ A:α    &   ⊢ R⊧[A = B]    ⇒   ⊢ B:α
Theorem	eqcomi 79	Commutativity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ A:α    &   ⊢ R⊧[A = B]    ⇒   ⊢ R⊧[B = A]
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.)
⊢ A:α    &   ⊢ R⊧[B = A]    ⇒   ⊢ B:α
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.)
⊢ A:α    &   ⊢ R⊧[B = A]    ⇒   ⊢ B:α
Theorem	mpbi 82	Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R⊧A    &   ⊢ R⊧[A = B]    ⇒   ⊢ R⊧B
Theorem	eqid 83	Reflexivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R:∗    &   ⊢ A:α    ⇒   ⊢ R⊧[A = A]
Theorem	ded 84	Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ (R, S)⊧T    &   ⊢ (R, T)⊧S    ⇒   ⊢ R⊧[S = T]
Theorem	dedi 85	Deduction theorem for equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ S⊧T    &   ⊢ T⊧S    ⇒   ⊢ ⊤⊧[S = T]
Theorem	eqtru 86	If a statement is provable, then it is equivalent to truth. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ R⊧A    ⇒   ⊢ R⊧[⊤ = A]
Theorem	mpbir 87	Deduction from equality inference. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ R⊧A    &   ⊢ R⊧[B = A]    ⇒   ⊢ R⊧B
Theorem	ceq12 88	Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → β)    &   ⊢ A:α    &   ⊢ R⊧[F = T]    &   ⊢ R⊧[A = B]    ⇒   ⊢ R⊧[(FA) = (TB)]
Theorem	ceq1 89	Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → β)    &   ⊢ A:α    &   ⊢ R⊧[F = T]    ⇒   ⊢ R⊧[(FA) = (TA)]
Theorem	ceq2 90	Equality theorem for combination. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → β)    &   ⊢ A:α    &   ⊢ R⊧[A = B]    ⇒   ⊢ R⊧[(FA) = (FB)]
Theorem	leq 91*	Equality theorem for lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    &   ⊢ R⊧[A = B]    ⇒   ⊢ R⊧[λx:α A = λx:α B]
Theorem	beta 92	Axiom of beta-substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:β    ⇒   ⊢ ⊤⊧[(λx:α Ax:α) = A]
Theorem	distrc 93	Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ F:(β → γ)    &   ⊢ A:β    &   ⊢ B:α    ⇒   ⊢ ⊤⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]
Theorem	distrl 94*	Distribution of lambda abstraction over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
⊢ A:γ    &   ⊢ B:α    ⇒   ⊢ ⊤⊧[(λx:α λy:β AB) = λy:β (λx:α AB)]
Theorem	eqtri 95	Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ A:α    &   ⊢ R⊧[A = B]    &   ⊢ R⊧[B = C]    ⇒   ⊢ R⊧[A = C]
Theorem	3eqtr4i 96	Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ A:α    &   ⊢ R⊧[A = B]    &   ⊢ R⊧[S = A]    &   ⊢ R⊧[T = B]    ⇒   ⊢ R⊧[S = T]
Theorem	3eqtr3i 97	Transitivity of equality. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ A:α    &   ⊢ R⊧[A = B]    &   ⊢ R⊧[A = S]    &   ⊢ R⊧[B = T]    ⇒   ⊢ R⊧[S = T]
Theorem	oveq123 98	Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[F = S]    &   ⊢ R⊧[A = C]    &   ⊢ R⊧[B = T]    ⇒   ⊢ R⊧[[AFB] = [CST]]
Theorem	oveq1 99	Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[A = C]    ⇒   ⊢ R⊧[[AFB] = [CFB]]
Theorem	oveq12 100	Equality theorem for binary operation. (Contributed by Mario Carneiro, 7-Oct-2014.)
⊢ F:(α → (β → γ))    &   ⊢ A:α    &   ⊢ B:β    &   ⊢ R⊧[A = C]    &   ⊢ R⊧[B = T]    ⇒   ⊢ R⊧[[AFB] = [CFT]]