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

Definition df-an 128
 Description: Define the 'and' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-an ⊤⊧[ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
Distinct variable group:   f,p,q

Detailed syntax breakdown of Definition df-an
StepHypRef Expression
1 kt 8 . 2 term
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 [⊤f:(∗ → (∗ → ∗))⊤]
157, 8, 14kl 6 . . . . . 6 term λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]
16 ke 7 . . . . . 6 term =
1713, 15, 16kbr 9 . . . . 5 term [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
183, 5, 17kl 6 . . . 4 term λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
193, 4, 18kl 6 . . 3 term λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
202, 19, 16kbr 9 . 2 term [ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
211, 20wffMMJ2 11 1 wff ⊤⊧[ = λp:∗ λq:∗ [λf:(∗ → (∗ → ∗)) [p:∗f:(∗ → (∗ → ∗))q:∗] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
 Colors of variables: type var term This definition is referenced by:  wan  136  anval  148
 Copyright terms: Public domain W3C validator