QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-b1 GIF version

Definition df-b1 1048
Description: Define biconditional for 1 . (Contributed by Roy F. Longton, 27-Jun-2005.)
Assertion
Ref Expression
df-b1 (a1 b) = ((a1 b) ∩ (b1 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  (a1 b)
41, 2wi1 12 . . 3 term  (a1 b)
52, 1wi1 12 . . 3 term  (b1 a)
64, 5wa 7 . 2 term  ((a1 b) ∩ (b1 a))
73, 6wb 1 1 wff  (a1 b) = ((a1 b) ∩ (b1 a))
Colors of variables: term
This definition is referenced by:  lem3.3.3  1052  lem3.3.5  1055
  Copyright terms: Public domain W3C validator