QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-b1 Unicode version
Definition df-b1 1048
Description: Define biconditional for ->1.
Assertion
Ref Expression
df-b1 (a <->1 b) = ((a ->1 b) ^ (b ->1 a))
Detailed syntax breakdown of Definition df-b1
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wb1 24 . 2 term (a <->1 b)
41, 2wi1 12 . . 3 term (a ->1 b)
52, 1wi1 12 . . 3 term (b ->1 a)
64, 5wa 7 . 2 term ((a ->1 b) ^ (b ->1 a))
73, 6wb 1 1 wff (a <->1 b) = ((a ->1 b) ^ (b ->1 a))
Colors of variables: term
This definition is referenced by:  lem3.3.3  1052  lem3.3.5  1055
  Copyright terms: Public domain W3C validator