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

Definition df-b 39
Description: Define biconditional. (Contributed by NM, 9-Aug-1997.)
Assertion
Ref Expression
df-b (ab) = ((ab ) ∪ (ab) )

Detailed syntax breakdown of Definition df-b
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
31, 2tb 5 . 2 term  (ab)
41wn 4 . . . . 5 term  a
52wn 4 . . . . 5 term  b
64, 5wo 6 . . . 4 term  (ab )
76wn 4 . . 3 term  (ab )
81, 2wo 6 . . . 4 term  (ab)
98wn 4 . . 3 term  (ab)
107, 9wo 6 . 2 term  ((ab ) ∪ (ab) )
113, 10wb 1 1 wff  (ab) = ((ab ) ∪ (ab) )
Colors of variables: term
This definition is referenced by:  dfb  94  wa6  196  r3a  440
  Copyright terms: Public domain W3C validator