Theorem 3anass 862

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 860	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		anass 487	. 2 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
3	1, 2	bitri 190	1 |- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3anrot 863  3exdistr 1693  3exdistrOLD 1694  eeeanvOLD 1709  mopick2OLD 1838  r3al 2151  ceqsex2 2326  ceqsex3v 2330  ceqsex4v 2331  ceqsex6v 2332  ceqsex8v 2333  trel3 3420  trssord 3675  ordelord 3680  dflim2 3719  dflim3 3930  dflim4 3932  brinxp2 4057  fncnv 4479  iunfopab 4542  dff1o2 4639  dff1o2OLD 4640  dff1o4 4644  dff1o4OLD 4645  f1ocnvOLD 4652  ndmoprass 4981  ndmoprdistr 4982  ecopoprtrn 5370  elixp2 5408  elixp 5409  zorn2lem7 5956  distrpq 6219  ltexpq 6232  distrlem3pr 6281  divmuldiv 6956  dfnn2 7119  sup3 7261  prime 7407  elioo1 7545  elioo2 7546  elioo3g 7547  elioc1 7548  elico1 7549  elicc1 7550  elioo5 7552  elioc2 7558  elico2 7559  elicc2 7560  ioossicc 7566  iccneg 7576  icoshft 7577  icounlem 7581  snunioolem 7583  ioojoin 7585  eluz2 7590  raluz2 7612  elfz1 7640  elfz 7641  elfz2 7642  fzsuc 7678  climcmplem 8397  iserzcmp0 8403  efcn 8688  istps3 8877  neindisj 9007  bl2ioo 9189  lmbrf 9208  lmclim 9241  bcthlem14 9290  bcthlem31 9307  issubg 9425  ajval 9863  pilem1 10020  pilem3 10022  grothprim 10141  cdrci 10182  abfi 10215  uptx 10226  h2hlm 10482  adjval 11451  dmadjss 11456  eleigvec 11518  bnj174 12042  bnj175 12044  bnj176 12045  bnj249 12088  bnj254 12093  bnj255 12094  bnj1197 12973  bnj1209 12983  bnj1275 13032  bnj1438 13132  bnj1506 13166  bnj543 13269  bnj571 13289  bnj583 13296  bnj607 13304  bnj849 13318  bnj882 13320  bnj983 13357  bnj987 13361  bnj1004 13369  bnj1033 13384  bnj1067 13399  bnj1097 13412  bnj1100 13414  bnj1145 13431  bnj1174 13442  elfzm11 13604  zmodid2 13614  lediv2aALT 13621  zgt1b2 13772  tfrALTlem 13976  nocvxminlem 14028  axfelem9 14039  df3nandALT2 14147  andnand1 14148  and4com 14267  ficli 14353  svs2 14829  svs3 14830  hmeogrp 14892  isalg 15068  algi 15074  ishomb 15137  cinvlem3 15178  settrcon 15247  tarval2 15249  isline1 15294  ivthALT 15454  filssufillem 15570  fmfnfm 15598  fzsplit 15792  sdc 15811  tlmbrf 15905  abl4pnp 16037  pi1val 16094  pi1gp 16095  isidl 16162  ispridl 16182  pridlidl 16183  pridlnr 16184  ismaxidl 16188  maxidlidl 16189  isfldidl2 16217  isdmn3 16222  iotasbc2 16384  isposNEW 16773  isopos 16909  cvrfval 16987  cvrval 16988  isgrpNEW 17104  grpclNEW 17106  isringNEW 17142  ringclNEW 17144  issrng 17176  islvec 17188  isphil 17195

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 164  df-an 242  df-3an 860

Copyright terms: Public domain