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

Definition df-b3 56
Description: Defined biconditional. (Contributed by NM, 2-Nov-1997.)
Assertion
Ref Expression
df-b3 (a3 b) = ((a3 b) ∩ (b3 a))

Detailed syntax breakdown of Definition df-b3
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
31, 2wb3 23 . 2 term  (a3 b)
41, 2wi3 14 . . 3 term  (a3 b)
52, 1wi3 14 . . 3 term  (b3 a)
64, 5wa 7 . 2 term  ((a3 b) ∩ (b3 a))
73, 6wb 1 1 wff  (a3 b) = ((a3 b) ∩ (b3 a))
Colors of variables: term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator