Theorem 3anass 777

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 775	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		anass 439	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
3	1, 2	bitr 173	1 |- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:   <-> wb 146   /\ wa 223   /\ w3a 773

This theorem is referenced by:  3anrot 778  3exdistr 1307  eeeanv 1319  mopick2 1429  r3al 1682  trel3 2678  trssord 2955  ordelord 2960  dflim2 3015  dflim4 3109  find 3145  brinxp2 3221  fncnv 3547  f1o2 3678  f1o4 3681  f1ocnv 3686  ndmoprass 4034  ndmoprdistr 4035  ecopoprtrn 4295  elixp2 4333  elixp 4334  zorn2lem7 4766  distrpq 5039  ltexpq 5052  distrlem3pr 5101  divdivdivt 5741  dfnn2 5884  sup3 5999  primet 6142  elioo1t 6315  elioo2t 6316  elioo3g 6317  elioc1t 6319  elico1t 6320  elicc1t 6321  elioc2t 6322  elico2t 6323  elicc2t 6324  ioossicc 6330  ioonegt 6339  iccnegt 6340  icoshft 6341  icounlem 6345  snunioolem 6347  eluz2t 6353  raluz2 6375  elfz1t 6402  elfzt 6403  elfz2t 6404  climcmplem 7073  iserzcmp0 7079  efsubt 7313  efcn 7363  istps3 7550  neindisj 7672  bl2ioo 7850  lmbrf 7868  lmclim 7898  bcthlem14 7946  bcthlem31 7963  issubg 8053  pilem1 8590  pilem3 8592  pigt2lt4 8594  grothprim 8722  h2hlm 8789  adjvalt 9731  dmadjss 9736  eleigvect 9797  lediv2itALT 10276  abfi 10349  ficli 10368  cdrci 10381  hmeogrp 10425  isalg 10497  algi 10504  ishomb 10560

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain