Theorem 3anass 969

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

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

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 967	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 649	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 249	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   /\ wa 369   /\ w3a 965

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967

This theorem is referenced by:  3anrot  970  3anan12  978  anandi3  979  3biant1d  1328  an33rean  1333  3exdistr  1941  r3al  2892  ceqsex2  3116  ceqsex3v  3118  ceqsex4v  3119  ceqsex6v  3120  ceqsex8v  3121  2reu5lem1  3272  2reu5lem2  3273  2reu5lem3  3274  eldifpr  4005  trel3  4504  ordelord  4852  dflim2  4886  dff1o4  5760  ndmovass  6364  ndmovdistr  6365  dflim3  6571  dflim4  6572  mpt2xopovel  6850  dfsmo2  6921  oeeui  7154  ecopovtrn  7316  elixp2  7380  elixp  7383  mptelixpg  7413  zorn2lem7  8785  grothprim  9115  grothtsk  9116  divmuldiv  10145  sup3  10401  dfnn3  10450  prime  10836  eluz2  10981  uzletr  10983  raluz2  11018  elixx1  11423  elixx3g  11427  elioo2  11455  elioo5  11467  elicc4  11476  iccneg  11526  icoshft  11527  difreicc  11537  elfz1  11562  elfz  11563  elfz2  11564  elfz2nn0  11600  elfzm11  11648  elfzo2  11676  elfzo3  11688  lbfzo0  11706  fzind2  11757  zmodid2  11856  swrdvalodm2  12454  swrdvalodm  12455  wrdeqswrdlsw  12464  swrdccatin1  12495  swrdccat  12505  repswswrd  12543  swrdco  12586  2swrd2eqwrdeq  12674  rediv  12741  imdiv  12748  cosmul  13578  bitsval  13741  bitsmod  13753  bitscmp  13755  smueqlem  13807  elgz  14113  xpsfrnel  14623  xpsfrnel2  14625  ismre  14650  mreexexlem4d  14707  iscatd2  14741  isssc  14855  eldmcoa  15055  isdrs  15226  isipodrs  15453  ismhm  15588  mhmpropd  15592  issubm  15597  submacs  15615  issubg  15803  eqglact  15854  eqgid  15855  pgrpsubgsymgbi  16034  isslw  16231  efgsdm  16351  mulgmhm  16439  mulgghm  16440  dmdprd  16605  dprdw  16619  dprdwOLD  16625  subgdmdprd  16656  dmdprdpr  16673  issrg  16734  srglmhm  16759  srgrmhm  16760  isrng  16775  rnglghm  16819  dfrhm2  16934  issubrg3  17019  islmod  17078  lsspropd  17224  islmhm  17234  islbs  17283  lbspropd  17306  isphl  18185  elocv  18221  isobs  18273  ma1repvcl  18511  smadiadetr  18616  istps3OLD  18662  neindisj  18856  lmbrf  18999  hauscmplem  19144  llyi  19213  subislly  19220  uptx  19333  txcn  19334  qtopeu  19424  elmptrab  19535  isfbas  19537  trfil2  19595  flimcls  19693  cnextcn  19774  psmettri2  20020  xmetec  20144  metuel2  20289  ngppropd  20358  bl2ioo  20504  xrtgioo  20518  om1elbas  20739  elpi1  20752  isclm  20771  iscph  20824  tchcph  20887  lmmbr2  20905  lmmbrf  20908  iscau2  20923  caussi  20943  lmclim  20948  bcthlem1  20970  srabn  21007  ishl2  21017  evthicc2  21079  ovolfioo  21086  ovolficc  21087  iblcnlem1  21401  iblrelem  21404  iblre  21407  iblcn  21412  isuc1p  21748  ismon1p  21750  ellogrn  22147  logreclem  22350  atandm  22407  atandm2  22408  atandm3  22409  atans2  22462  dmarea  22487  dchrelbas4  22718  ax5seg  23356  eengtrkg  23403  nbgrael  23509  nb3grapr2  23534  wlks  23597  wlkon  23601  trls  23607  is2wlk  23636  pths  23637  0pth  23641  isgrpo2  23856  issubgo  23962  ajval  24434  issh  24782  dmadjss  25463  adjeu  25465  adjval  25466  isst  25789  ishst  25790  xrdifh  26235  nndiffz1  26240  xdivpnfrp  26273  isomnd  26329  omndmul2  26340  isslmd  26383  isrrext  26594  issibf  26883  eulerpartleme  26910  eulerpartlemt0  26916  probun  26966  erdszelem1  27243  cvmsval  27319  cvmliftiota  27354  snmlval  27384  lediv2aALT  27486  elwlim  27924  nocvxminlem  27995  nofulllem1  28007  nofulllem5  28011  brtxp2  28076  brpprod3a  28081  brcart  28127  brsuccf  28136  broutsideof3  28321  df3nandALT2  28408  andnand1  28409  fin2solem  28583  itg2gt0cn  28615  iblabsnclem  28623  areacirc  28657  ivthALT  28698  islocfin  28736  neificl  28817  ablo4pnp  28913  isrngohom  28939  isidl  28982  ispridl  29002  pridlidl  29003  ismaxidl  29008  maxidlidl  29009  isfldidl2  29037  isdmn3  29042  fz1eqin  29275  issdrg  29722  sdrgacs  29726  isdomn3  29740  iotasbc2  29842  stoweidlem17  29980  stoweidlem34  29997  stoweidlem60  30023  ndmaovass  30280  ndmaovdistr  30281  rexdifpr  30292  2elfz3nn0  30367  ccats1rev  30428  ccatw2s1p1  30437  ccatw2s1p2  30438  ccat2s1fvw  30439  2wlkeq  30456  usgra2pthspth  30463  usgra2adedgspthlem2  30472  usgra2adedgwlkon  30475  iswwlk  30485  wwlknimp  30489  wwlkextwrd  30528  2pthwlkonot  30572  usg2spthonot  30575  isclwwlk  30599  clwwlknprop  30603  clwwlkn2  30606  clwlkisclwwlklem0  30618  clwlkfclwwlk  30685  isrusgra  30712  rusgranumwlkl1  30727  rusgranumwlklem0  30734  1to3vfriswmgra  30767  numclwwlkovgel  30849  numclwwlk2lem1  30863  mat1dimscm  31057  lindslinindsimp2lem5  31148  mat2pmatghm  31239  mat2pmatmul  31240  decpmatmulsumfsupp  31280  pm2mpghm  31323  pm2mpmhmlem1  31325  alimp-no-surprise  31485  eelT00  31781  eelTTT  31782  eelT11  31784  eelT12  31788  eelTT1  31790  eelT01  31791  eel0T1  31792  uun132  31870  uun132p1  31871  un2122  31875  uunTT1  31878  uunTT1p1  31879  uunTT1p2  31880  uunT11  31881  uunT11p1  31882  uunT11p2  31883  uunT12  31884  uunT12p1  31885  uunT12p2  31886  uunT12p3  31887  uunT12p4  31888  uunT12p5  31889  uun111  31890  uun2221  31898  uun2221p1  31899  uun2221p2  31900  bnj250  32041  bnj255  32045  bnj345  32054  bnj945  32119  bnj1209  32142  bnj1275  32159  bnj543  32238  bnj571  32251  bnj607  32261  bnj882  32271  bnj983  32296  bnj996  32300  bnj1006  32304  bnj1033  32312  bnj1097  32324  bnj1110  32325  bnj1145  32336  bnj1174  32346  bnj1189  32352  bnj1450  32393  bnj1514  32406  islshp  32982  isopos  33183  cvrfval  33271  cvrval  33272  isatl  33302  isat3  33310  islpln5  33537  4atlem11  33611  dalem20  33695  lhpexle3  34014  lhpex2leN  34015  isltrn2N  34122  diclspsn  35197  lcfls1lem  35537  lcfls1N  35538