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

Definition df-or 132
 Description: Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-or
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 kt 8 . 2 term
2 tor 124 . . 3 term
3 hb 3 . . . 4 type
4 vp . . . 4 var
5 vq . . . . 5 var
6 tal 122 . . . . . 6 term
7 vx . . . . . . 7 var
83, 4tv 1 . . . . . . . . 9 term
93, 7tv 1 . . . . . . . . 9 term
10 tim 121 . . . . . . . . 9 term
118, 9, 10kbr 9 . . . . . . . 8 term
123, 5tv 1 . . . . . . . . . 10 term
1312, 9, 10kbr 9 . . . . . . . . 9 term
1413, 9, 10kbr 9 . . . . . . . 8 term
1511, 14, 10kbr 9 . . . . . . 7 term
163, 7, 15kl 6 . . . . . 6 term
176, 16kc 5 . . . . 5 term
183, 5, 17kl 6 . . . 4 term
193, 4, 18kl 6 . . 3 term
20 ke 7 . . 3 term
212, 19, 20kbr 9 . 2 term
221, 21wffMMJ2 11 1 wff
 Colors of variables: type var term This definition is referenced by:  wor  140  orval  147
 Copyright terms: Public domain W3C validator