Let us present other useful connectives, with their properties true for all possible values of the Boolean variables (A, B, C, that can be replaced by formulas).
¬1 ¬0 ¬(¬A) 
⇔ 0 ⇔ 1 ⇔ A 
x ≠ y x ∉ E (A ⇎ B) (A ⇎ B) 
⇔ ¬(x=y) ⇔ ¬(x ∈ E) ⇔ ¬(A ⇔ B) ⇔ (A ⇔ ¬B)) 
(x is not equal to y) (x is not an element of E) (Inequivalence) 
Idempotent (A ∧ A) ⇔ A (A ∨ A) ⇔ A 
Commutative (B ∧ A) ⇔ (A ∧ B)
(B ∨ A) ⇔ (A ∨ B) 
Associative ((A ∧ B) ∧ C) ⇔ (A
∧ (B ∧ C))
((A ∨ B) ∨ C) ⇔ (A ∨ (B ∨ C)) 
Distributive over the other (A ∧ (B ∨ C)) ⇔ ((A
∧ B) ∨ (A ∧ C))
(A ∨ (B ∧ C)) ⇔ ((A ∨ B) ∧ (A ∨ C)) 
(A ∨ B)
⇎ (¬A ∧ ¬B)
(A ∧ B) ⇎ (¬A ∨ ¬B)
Asserting a conjunction of formulas amounts to successively asserting all these formulas.
The inequivalence ⇎ is also called «exclusive or» because (A ⇎ B) can also be written ((A ∨ B) ∧ ¬(A ∧ B)).(A ⇒ B) ⇎ (A ⇒ B) ⇔ 
(A ∧ ¬B) (¬B ⇒ ¬A) 
The formula (A ∧ (A ⇒ B)) will be abbreviated as A ∴ B, which reads «A therefore B». It is equivalent to (A ∧ B), but indicating that it is deduced from the truths of A and (A ⇒ B).
Negations transform the associativity and distributivity formulas of conjunctions and disjunctions, into various formulas with implications:
In a different kind of abbreviation, any string of formulas linked by ⇔ and/or ⇒ will mean the conjunction of all these implications or equivalences between adjacent formulas:
(A ⇒ B
⇒ C) ⇔ ((A ⇒ B) ∧ (B ⇒ C)) ⇒
(A ⇒ C)
(A ⇔ B ⇔ C) ⇔ ((A ⇔ B) ∧ (B
⇔ C)) ⇒ (A ⇔ C)
0 ⇒ A ⇒ A ⇒ 1
(¬A) ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ∧ 1) ⇔ A ⇔ (A ∨ 0) ⇔ (1 ⇒ A) ⇔ (A
⇔ 1)
(A ∧ B) ⇒ A
⇒ (A ∨ B)
x = y ⇒ x = y ⇒ 
x = x T(x) = T(y) (A(x) ⇔ A(y)) 
(A ∧
¬A) ⇔ 0
((T⊢ A)∧(T⊢ ¬A))⇔(T⊢ 0).
Without trying to formalize what a proof is, we shall just write
proofs naturally, usually as a succession of formulas, each visibly
true thanks to previous ones and the above properties of connectives
and equality. Natural language articulations may also appear,
especially when dealing with quantifiers
(1.9) and introducing symbols defined by expressions.
In particular, an equality between terms x = y
allows to replace any occurrence of x by y in any
expression without affecting the result; when a symbol is defined by
a term, both are equal, thus can be substituted to each other in any
expression. Axioms and other rules expressed with variable symbols
(under universal quantifiers, see 1.9) can then be used replacing
these variables by terms.
Provable
formulas with a known proof (either by humans or by
computers) can be differently named in usual language according to their
importance: a theorem is more important than a proposition; either of them
may be deduced from an otherwise less important lemma, and a corollary may be
easily deduced from it.
Set theory and Foundations of Mathematics  
1. First
foundations of mathematics 
1.6. Logical connectives
⇨ 1.7. Classes
in set theory 1.8. Binders
in set theory
1.9. Quantifiers 1.10. Formalization of set theory 1.11. Set generation principle 

Philosophical aspects  ⇨ Time in model theory  Interpretation
of classes Concepts of truth in mathematics 
2. Set theory (continued)  3. Algebra  4. Model theory 