QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-i5 Structured version   Unicode version

Definition df-i5 48
Description: Define relevance conditional.
Assertion
Ref Expression
df-i5 (a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))

Detailed syntax breakdown of Definition df-i5
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wi5 16 . 2 term (a ->5 b)
41, 2wa 7 . . . 4 term (a ^ b)
51wn 4 . . . . 5 term a'
65, 2wa 7 . . . 4 term (a' ^ b)
74, 6wo 6 . . 3 term ((a ^ b) v (a' ^ b))
82wn 4 . . . 4 term b'
95, 8wa 7 . . 3 term (a' ^ b')
107, 9wo 6 . 2 term (((a ^ b) v (a' ^ b)) v (a' ^ b'))
113, 10wb 1 1 wff (a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
Colors of variables: term
This definition is referenced by:  ud5lem0a  264  ud5lem0b  265  i5con  272  ud5lem0c  281  nom15  312  i5lei1  347  i5lei2  348  i5lei3  349  i5lei4  350  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem2  590  ud5lem3a  591  ud5lem3  594  u5lemaa  604  u5lemana  609  u5lemab  614  u5lemanb  619  u5lemoa  624  u5lemona  629  u5lemob  634  u5lemonb  639  u5lemc1  684  u5lemc1b  685  u5lemc2  690  u5lemc4  705  u5lemle2  719  u5lembi  725  u5lem5  765  u5lem6  769  u24lem  770  lem3.3.7i5e1  1072  wdwom  1104
  Copyright terms: Public domain W3C validator