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

Axiom ax-distrc 68
 Description: Distribution of combination over substitution. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-beta.1 A:β
ax-distrc.2 B:α
ax-distrc.3 F:(βγ)
Assertion
Ref Expression
ax-distrc ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))

Detailed syntax breakdown of Axiom ax-distrc
StepHypRef Expression
1 kt 8 . 2 term
2 ke 7 . . . 4 term =
3 hal . . . . . 6 type α
4 vx . . . . . 6 var x
5 tf . . . . . . 7 term F
6 ta . . . . . . 7 term A
75, 6kc 5 . . . . . 6 term (FA)
83, 4, 7kl 6 . . . . 5 term λx:α (FA)
9 tb . . . . 5 term B
108, 9kc 5 . . . 4 term (λx:α (FA)B)
112, 10kc 5 . . 3 term ( = (λx:α (FA)B))
123, 4, 5kl 6 . . . . 5 term λx:α F
1312, 9kc 5 . . . 4 term (λx:α FB)
143, 4, 6kl 6 . . . . 5 term λx:α A
1514, 9kc 5 . . . 4 term (λx:α AB)
1613, 15kc 5 . . 3 term ((λx:α FB)(λx:α AB))
1711, 16kc 5 . 2 term (( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
181, 17wffMMJ2 11 1 wff ⊤⊧(( = (λx:α (FA)B))((λx:α FB)(λx:α AB)))
 Colors of variables: type var term This axiom is referenced by:  distrc  93
 Copyright terms: Public domain W3C validator