HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-distrc Unicode 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:be
ax-distrc.2 |- B:al
ax-distrc.3 |- F:(be -> ga)
Assertion
Ref Expression
ax-distrc |- T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))

Detailed syntax breakdown of Axiom ax-distrc
StepHypRef Expression
1 kt 8 . 2 term T.
2 ke 7 . . . 4 term =
3 hal . . . . . 6 type al
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:al (FA)
9 tb . . . . 5 term B
108, 9kc 5 . . . 4 term (\x:al (FA)B)
112, 10kc 5 . . 3 term ( = (\x:al (FA)B))
123, 4, 5kl 6 . . . . 5 term \x:al F
1312, 9kc 5 . . . 4 term (\x:al FB)
143, 4, 6kl 6 . . . . 5 term \x:al A
1514, 9kc 5 . . . 4 term (\x:al AB)
1613, 15kc 5 . . 3 term ((\x:al FB)(\x:al AB))
1711, 16kc 5 . 2 term (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
181, 17wffMMJ2 11 1 wff T. |= (( = (\x:al (FA)B))((\x:al FB)(\x:al AB)))
Colors of variables: type var term
This axiom is referenced by:  distrc  93
  Copyright terms: Public domain W3C validator