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

Definition df-an 128
Description: Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-an |- T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Distinct variable group:   f,p,q

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 kt 8 . 2 term T.
2 tan 119 . . 3 term /\
3 hb 3 . . . 4 type *
4 vp . . . 4 var p
5 vq . . . . 5 var q
63, 3ht 2 . . . . . . . 8 type (* -> *)
73, 6ht 2 . . . . . . 7 type (* -> (* -> *))
8 vf . . . . . . 7 var f
93, 4tv 1 . . . . . . . 8 term p:*
103, 5tv 1 . . . . . . . 8 term q:*
117, 8tv 1 . . . . . . . 8 term f:(* -> (* -> *))
129, 10, 11kbr 9 . . . . . . 7 term [p:*f:(* -> (* -> *))q:*]
137, 8, 12kl 6 . . . . . 6 term \f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*]
141, 1, 11kbr 9 . . . . . . 7 term [T.f:(* -> (* -> *))T.]
157, 8, 14kl 6 . . . . . 6 term \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]
16 ke 7 . . . . . 6 term =
1713, 15, 16kbr 9 . . . . 5 term [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
183, 5, 17kl 6 . . . 4 term \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
193, 4, 18kl 6 . . 3 term \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
202, 19, 16kbr 9 . 2 term [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
211, 20wffMMJ2 11 1 wff T. |= [ /\ = \p:* \q:* [\f:(* -> (* -> *)) [p:*f:(* -> (* -> *))q:*] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
Colors of variables: type var term
This definition is referenced by:  wan  136  anval  148
  Copyright terms: Public domain W3C validator