Definition df-ov 285

Description: Definition of operator application. It's simply two curried function applications.

Assertion

Ref	Expression
df-ov	⊦ (AFB) = ((F' A)' B)

Detailed syntax breakdown of Definition df-ov

Step	Hyp	Ref	Expression
1		na	. . 3 nilad A
2		nb	. . 3 nilad B
3		nf	. . 3 nilad F
4	1, 2, 3	nov 284	. 2 nilad (AFB)
5	3, 1	nfv 281	. . 3 nilad (F' A)
6	5, 2	nfv 281	. 2 nilad ((F' A)' B)
7	4, 6	weq 246	1 wff (AFB) = ((F' A)' B)

This definition is referenced by: (None)