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

Definition df-ov 73
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. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
wov.1 |- F:(al -> (be -> ga))
wov.2 |- A:al
wov.3 |- B:be
Assertion
Ref Expression
df-ov |- T. |= (( = [AFB])((FA)B))

Detailed syntax breakdown of Definition df-ov
StepHypRef Expression
1 kt 8 . 2 term T.
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 T. |= (( = [AFB])((FA)B))
Colors of variables: type var term
This definition is referenced by:  dfov1  74  dfov2  75  oveq123  98  hbov  111  ovl  117
  Copyright terms: Public domain W3C validator