hbth - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > hbth		GIF version

Theorem hbth 99

Description: Hypothesis builder for a theorem.

**Hypotheses**
Ref	Expression
hbth.1	⊢ B:α
hbth.2	⊢ R⊧A

**Assertion**
Ref	Expression
hbth	⊢ R⊧[(λx:α AB) = A]

Distinct variable group: x,R

**Proof of Theorem hbth**
Step	Hyp	Ref	Expression
1		hbth.2	. . 3 ⊢ R⊧A
2	1	ax-cb2 30	. 2 ⊢ A:∗
3		hbth.1	. 2 ⊢ B:α
4		wtru 40	. . 3 ⊢ ⊤:∗
5	1	eqtru 76	. . 3 ⊢ R⊧[⊤ = A]
6	4, 5	eqcomi 70	. 2 ⊢ R⊧[A = ⊤]
7	1	ax-cb1 29	. . 3 ⊢ R:∗
8	4, 3, 7	a17i 96	. 2 ⊢ R⊧[(λx:α ⊤B) = ⊤]
9	2, 3, 6, 8	hbxfr 98	1 ⊢ R⊧[(λx:α AB) = A]

Colors of variables: type var term

Syntax hints: ∗hb 3 kc 5 λkl 6 = ke 7 ⊤kt 8 [kbr 9 ⊧wffMMJ2 11 wffMMJ2t 12

This theorem was proved from axioms: ax-syl 15 ax-jca 17 ax-simpl 20 ax-simpr 21 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-refl 39 ax-eqmp 42 ax-ded 43 ax-ceq 46 ax-leq 62 ax-17 95

This theorem depends on definitions: df-ov 65

This theorem is referenced by: ax4g 139