Theorem distrc 93

Description: Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
distrc.1	⊢ F:(β → γ)
distrc.2	⊢ A:β
distrc.3	⊢ B:α

Assertion

Ref	Expression
distrc	⊢ ⊤⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]

Proof of Theorem distrc

Step	Hyp	Ref	Expression
1		weq 41	. 2 ⊢ = :(γ → (γ → ∗))
2		distrc.1	. . . . 5 ⊢ F:(β → γ)
3		distrc.2	. . . . 5 ⊢ A:β
4	2, 3	wc 50	. . . 4 ⊢ (FA):γ
5	4	wl 66	. . 3 ⊢ λx:α (FA):(α → γ)
6		distrc.3	. . 3 ⊢ B:α
7	5, 6	wc 50	. 2 ⊢ (λx:α (FA)B):γ
8	2	wl 66	. . . 4 ⊢ λx:α F:(α → (β → γ))
9	8, 6	wc 50	. . 3 ⊢ (λx:α FB):(β → γ)
10	3	wl 66	. . . 4 ⊢ λx:α A:(α → β)
11	10, 6	wc 50	. . 3 ⊢ (λx:α AB):β
12	9, 11	wc 50	. 2 ⊢ ((λx:α FB)(λx:α AB)):γ
13	3, 6, 2	ax-distrc 68	. 2 ⊢ ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
14	1, 7, 12, 13	dfov2 75	1 ⊢ ⊤⊧[(λx:α (FA)B) = ((λx:α FB)(λx:α AB))]

This proof depends on syntax axioms:   → ht 2  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12

This proof depends on axioms:  ax-syl 15  ax-jca 17  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-wc 49  ax-ceq 51  ax-wl 65  ax-distrc 68  ax-wov 71

This proof depends on definitions:  df-ov 73

This theorem is used by:  hbc  110