Theorem 3anass 585

Description: Associative law for triple conjunction.

Assertion

Ref	Expression
3anass	|- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 583	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		anass 336	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
3	1, 2	bitr 151	1 |- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:   <-> wb 127   /\ wa 196   /\ w3a 581

This theorem is referenced by:  3anrot 586  3exdistr 970  eeeanv 981  mopick2 1057  r3al 1240  trel3 2049  so 2152  trssord 2216  ordelord 2221  dflim2 2280  find 2396  f1o2 2804  f1o4 2807  f1ocnv 2811  f1oco 2816  ndmoprass 3062  ndmoprdistr 3063  ecopoprtrn 3247  zornlem7 3609  distrpq 3861  ltexpq 3874  distrlem3pr 3923  divdivdivt 4265  recdivt 4270  sup3 4511

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org