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

Definition df-ov 65
 Description: 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.
Hypotheses
Ref Expression
wov.1 F:(α → (βγ))
wov.2 A:α
wov.3 B:β
Assertion
Ref Expression
df-ov ⊤⊧(( = [AFB])((FA)B))

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 kt 8 . 2 term
2 ke 7 . . . 4 term =
3 ta . . . . 5 term A
4 tb . . . . 5 term B
5 tf . . . . 5 term F
63, 4, 5kbr 9 . . . 4 term [AFB]
72, 6kc 5 . . 3 term ( = [AFB])
85, 3kc 5 . . . 4 term (FA)
98, 4kc 5 . . 3 term ((FA)B)
107, 9kc 5 . 2 term (( = [AFB])((FA)B))
111, 10wffMMJ2 11 1 wff ⊤⊧(( = [AFB])((FA)B))
 Colors of variables: type var term This definition is referenced by:  dfov1  66  dfov2  67  oveq123  88  hbov  101  ovl  107
 Copyright terms: Public domain W3C validator