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

Step	Hyp	Ref	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
6	3, 4, 5	kbr 9	. . . 4 term [AFB]
7	2, 6	kc 5	. . 3 term ( = [AFB])
8	5, 3	kc 5	. . . 4 term (FA)
9	8, 4	kc 5	. . 3 term ((FA)B)
10	7, 9	kc 5	. 2 term (( = [AFB])((FA)B))
11	1, 10	wffMMJ2 11	1 wff T. |= (( = [AFB])((FA)B))

This definition is referenced by:  dfov1  74  dfov2  75  oveq123  98  hbov  111  ovl  117