Metamath Proof Explorer

Definition df-3an

Description: Define conjunction ('and') of three wff's. Definition *4.34 of WhiteheadRussell p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass . (Contributed by NM, 8-Apr-1994)

Ref Expression
Assertion df-3an φ ψ χ φ ψ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 w3a wff φ ψ χ
4 0 1 wa wff φ ψ
5 4 2 wa wff φ ψ χ
6 3 5 wb wff φ ψ χ φ ψ χ