Theorem 3anass 995

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 993	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 659	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 257	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 189   /\ wa 375   /\ w3a 991

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 190  df-an 377  df-3an 993

This theorem is referenced by:  3anrot  996  3anan12  1004  anandi3  1005  3biant1d  1388  an33rean  1393  cad1  1530  3exdistr  1850  r3alOLD  2838  ceqsex2  3098  ceqsex3v  3100  ceqsex4v  3101  ceqsex6v  3102  ceqsex8v  3103  2reu5lem1  3257  2reu5lem2  3258  2reu5lem3  3259  eldifpr  4002  trel3  4519  2rbropap  4756  ordelord  5464  dflim2  5498  dff1o4  5845  fvmptopab2  6360  brfvopab  6363  ndmovass  6484  ndmovdistr  6485  dflim3  6701  dflim4  6702  mpt2xopovel  6993  dfsmo2  7092  dfrecs3  7117  oeeui  7329  ecopovtrn  7492  elixp2  7552  elixp  7555  mptelixpg  7585  eqinf  8026  zorn2lem7  8958  grothprim  9285  grothtsk  9286  divmuldiv  10335  sup3  10594  dfnn3  10651  prime  11045  eluz2  11194  raluz2  11237  elixx1  11673  elixx3g  11677  elioo2  11706  elioo5  11721  elicc4  11730  iccneg  11782  icoshft  11783  difreicc  11793  elfz1  11818  elfz  11819  elfz2  11820  elfzm11  11894  elfz2nn0  11914  elfzo2  11954  elfzo3  11967  lbfzo0  11986  fzind2  12054  zmodid2  12157  swrdnd2  12826  swrdccatin1  12876  swrdccat  12886  repswswrd  12924  swrdco  12971  2swrd2eqwrdeq  13077  ccat2s1fvwALT  13079  rediv  13243  imdiv  13250  cosmul  14276  bitsval  14446  bitsmod  14459  bitscmp  14461  smueqlem  14513  lcmneg  14617  lcmftp  14658  coprmgcdb  14703  elgz  14924  xpsfrnel  15518  xpsfrnel2  15520  ismre  15545  mreexexlem4d  15602  iscatd2  15636  isssc  15774  eldmcoa  16009  isdrs  16228  isipodrs  16456  ismhm  16633  mhmpropd  16637  issubm  16643  submacs  16661  issubg  16866  eqglact  16917  eqgid  16918  pgrpsubgsymgbi  17097  isslw  17309  efgsdm  17429  mulgmhm  17517  mulgghm  17518  dmdprd  17679  dprdw  17691  subgdmdprd  17716  dmdprdpr  17731  issrg  17790  srglmhm  17817  srgrmhm  17818  isring  17833  ringlghm  17881  dfrhm2  17994  issubrg3  18085  islmod  18144  lsspropd  18289  islmhm  18299  islbs  18348  lbspropd  18371  isphl  19244  elocv  19280  isobs  19332  mat1dimscm  19549  scmatghm  19607  scmatmhm  19608  ma1repvcl  19644  smadiadetr  19749  mat2pmatghm  19803  mat2pmatmul  19804  decpmatmulsumfsupp  19846  pm2mpghm  19889  pm2mpmhmlem1  19891  neindisj  20182  lmbrf  20325  hauscmplem  20470  llyi  20538  subislly  20545  islocfin  20581  uptx  20689  txcn  20690  qtopeu  20780  elmptrab  20891  isfbas  20893  trfil2  20951  flimcls  21049  cnextcn  21131  xmetec  21498  ngppropd  21694  bl2ioo  21859  xrtgioo  21873  om1elbas  22112  elpi1  22125  isclm  22144  iscph  22197  tchcph  22260  lmmbr2  22278  lmmbrf  22281  iscau2  22296  caussi  22316  lmclim  22321  bcthlem1  22341  srabn  22376  ishl2  22386  evthicc2  22460  ovolfioo  22469  ovolficc  22470  iblcnlem1  22794  iblrelem  22797  iblre  22800  iblcn  22805  isuc1p  23140  ismon1p  23142  ellogrn  23558  logreclem  23748  atandm  23851  atandm2  23852  atandm3  23853  atans2  23906  dmarea  23932  dchrelbas4  24220  ax5seg  25017  eengtrkg  25064  nbgrael  25203  nb3grapr2  25231  wlks  25296  wlkon  25310  trls  25315  is2wlk  25344  pths  25345  0pth  25349  usgra2adedgspthlem2  25389  usgra2adedgwlkon  25392  iswwlk  25460  wwlknimp  25464  2wlkeq  25484  wwlkextwrd  25505  wwlkextinj  25507  isclwwlk  25545  clwwlknprop  25549  clwwlkn2  25552  clwlkisclwwlklem0  25565  clwlkfclwwlk  25621  2pthwlkonot  25662  usg2spthonot  25665  isrusgra  25704  isrusgusrg  25709  isrusgrac  25712  rusgranumwlkl1  25724  rusgranumwlklem0  25725  1to3vfriswmgra  25784  numclwwlkovgel  25865  numclwwlk2lem1  25879  isgrpo2  25974  issubgo  26080  ajval  26552  issh  26910  dmadjss  27589  adjeu  27591  adjval  27592  isst  27915  ishst  27916  xrdifh  28411  nndiffz1  28415  xdivpnfrp  28451  isomnd  28513  isslmd  28567  isrrext  28853  ismntop  28879  isros  29039  issros  29046  issibf  29215  eulerpartleme  29245  eulerpartlemt0  29251  probun  29301  bnj250  29555  bnj255  29559  bnj345  29568  bnj945  29634  bnj1209  29657  bnj1275  29674  bnj543  29753  bnj571  29766  bnj607  29776  bnj882  29786  bnj983  29811  bnj996  29815  bnj1006  29819  bnj1033  29827  bnj1097  29839  bnj1110  29840  bnj1145  29851  bnj1174  29861  bnj1189  29867  bnj1450  29908  bnj1514  29921  erdszelem1  29963  cvmsval  30038  cvmliftiota  30073  snmlval  30103  lediv2aALT  30370  elwlim  30555  nocvxminlem  30628  nofulllem1  30640  nofulllem5  30644  brtxp2  30697  brpprod3a  30702  brcart  30748  brsuccf  30757  broutsideof3  30942  ivthALT  31040  df3nandALT2  31107  andnand1  31108  topdifinffinlem  31795  relowlssretop  31811  rdgeqoa  31818  fin2solem  31976  poimirlem3  31988  poimirlem4  31989  poimirlem26  32011  poimirlem27  32012  poimirlem32  32017  itg2gt0cn  32042  iblabsnclem  32050  areacirc  32082  neificl  32127  ablo4pnp  32223  isrngohom  32249  isidl  32292  ispridl  32312  pridlidl  32313  ismaxidl  32318  maxidlidl  32319  isfldidl2  32347  isdmn3  32352  islshp  32590  isopos  32791  cvrfval  32879  cvrval  32880  isatl  32910  isat3  32918  islpln5  33145  4atlem11  33219  dalem20  33303  lhpexle3  33622  lhpex2leN  33623  isltrn2N  33730  diclspsn  34807  lcfls1lem  35147  lcfls1N  35148  fz1eqin  35656  issdrg  36108  sdrgacs  36112  isdomn3  36126  rp-isfinite6  36208  snhesn  36427  iotasbc2  36815  eelT00  37128  eelTTT  37129  eelT11  37130  eelT12  37134  eelTT1  37135  eelT01  37136  eel0T1  37137  uun132  37212  uun132p1  37213  un2122  37217  uunTT1  37220  uunTT1p1  37221  uunTT1p2  37222  uunT11  37223  uunT11p1  37224  uunT11p2  37225  uunT12  37226  uunT12p1  37227  uunT12p2  37228  uunT12p3  37229  uunT12p4  37230  uunT12p5  37231  uun111  37232  uun2221  37240  uun2221p1  37241  uun2221p2  37242  stoweidlem17  37915  stoweidlem34  37933  stoweidlem60  37959  ndmaovass  38746  ndmaovdistr  38747  reuccatpfxs1  39015  rexdifpr  39034  2elfz3nn0  39098  uspgredg2v  39351  nbgrel  39460  nb3grpr2  39507  isrusgr0  39633  rusgrprop0  39634  ewlkprop  39670  1wlksfval  39674  wlksfval  39675  wlkbProp  39680  wlkson  39707  wlkOnprop  39709  wlkOnwlk  39712  wlkOnwlk1l  39713  upgr2wlk  39715  upgrtrls  39736  upgristrl  39737  1wlksonproplem  39740  upgrwlkdvde  39769  pthOnpth  39780  isspthonpth-av  39781  spthonepeq-av  39784  uhgr1wlkspth  39787  usgr2wlkneq  39788  usgr2wlkspth  39791  0wlkOnlem1  39835  0pth-av  39841  21wlkond  39886  2pthond  39891  umgr2adedgwlk  39894  umgr2adedgwlkon  39895  umgr2adedgwlkonALT  39896  umgr2adedgspth  39897  usgra2pthspth  39938  isrng  40149  2zrngnmrid  40223  lindslinindsimp2lem5  40528  alimp-no-surprise  40793