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

Definition df-or 122
Description: Define the 'or' operator.
Assertion
Ref Expression
df-or |- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
Distinct variable group:   p,q,x

Detailed syntax breakdown of Definition df-or
StepHypRef Expression
1 kt 8 . 2 term T.
2 tor 114 . . 3 term \/
3 hb 3 . . . 4 type *
4 vp . . . 4 var p
5 vq . . . . 5 var q
6 tal 112 . . . . . 6 term A.
7 vx . . . . . . 7 var x
83, 4tv 1 . . . . . . . . 9 term p:*
93, 7tv 1 . . . . . . . . 9 term x:*
10 tim 111 . . . . . . . . 9 term ==>
118, 9, 10kbr 9 . . . . . . . 8 term [p:* ==> x:*]
123, 5tv 1 . . . . . . . . . 10 term q:*
1312, 9, 10kbr 9 . . . . . . . . 9 term [q:* ==> x:*]
1413, 9, 10kbr 9 . . . . . . . 8 term [[q:* ==> x:*] ==> x:*]
1511, 14, 10kbr 9 . . . . . . 7 term [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]
163, 7, 15kl 6 . . . . . 6 term \x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]
176, 16kc 5 . . . . 5 term (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])
183, 5, 17kl 6 . . . 4 term \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])
193, 4, 18kl 6 . . 3 term \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])
20 ke 7 . . 3 term =
212, 19, 20kbr 9 . 2 term [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
221, 21wffMMJ2 11 1 wff T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
Colors of variables: type var term
This definition is referenced by:  wor  130  orval  137
  Copyright terms: Public domain W3C validator