Definition df-3an 583

Description: Define conjunction ('and') of 3 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 336.

Assertion

Ref	Expression
df-3an	⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3		wch	. . 3 wff χ
4	1, 2, 3	w3a 581	. 2 wff (φ ∧ ψ ∧ χ)
5	1, 2	wa 196	. . 3 wff (φ ∧ ψ)
6	5, 3	wa 196	. 2 wff ((φ ∧ ψ) ∧ χ)
7	4, 6	wb 127	1 wff ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))

This definition is referenced by:  3anass 585  3anrot 586  3ancoma 588  3simpa 591  3pm3.2i 603  3jca 604  im3an 605  bi3an 606  3imp 608  3exp 611  bi3and 636  an6 638  hb3an 707  otthg 1900  poss 2129  poirr 2133  po2nr 2135  po3nr 2136  dfwe2 2187  wefrc 2195  f1orn 2809  tz7.49c 2998  ndmoprass 3062  oaord 3149  nnmord 3189  sup2 4510  infxpidmlem7 4939

metamath.org