Definition df-3an 1039

Description: Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 681. (Contributed by NM, 8-Apr-1994.)

Assertion

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

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	w3a 1037	. 2 wff ( ph /\ ps /\ ch )
5	1, 2	wa 384	. . 3 wff ( ph /\ ps )
6	5, 3	wa 384	. 2 wff ( ( ph /\ ps ) /\ ch )
7	4, 6	wb 196	1 wff ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

This definition is referenced by:  3anass  1042  3anrot  1043  3ancoma  1045  3anan32  1050  3anor  1054  3ioran  1056  3simpa  1058  3pm3.2i  1239  pm3.2an3  1240  pm3.2an3OLD  1241  3jca  1242  3anbi123i  1251  3imp  1256  3an4anass  1291  3anbi123d  1399  3anim123d  1406  an6  1408  an3andi  1445  an33rean  1446  cadan  1548  19.26-3an  1800  nf3and  1827  nf3an  1831  4exdistr  1924  eeeanv  2183  nf3andOLD  2233  nf3anOLD  2239  sb3an  2400  mopick2  2540  r3al  2940  r19.26-3  3066  3reeanv  3108  ceqsex3v  3246  ceqsex4v  3247  ceqsex8v  3249  sbc3an  3494  elin3  3804  rexdifpr  4205  raltpg  4236  tpss  4368  dfopif  4399  disjxun  4651  otth2  4952  otthg  4954  oteqex  4964  poirr  5046  po3nr  5049  wefrc  5108  rabxp  5154  brinxp2  5180  brinxp  5181  f1orn  6147  fpropnf1  6524  dff1o6  6531  oprabid  6677  oprabv  6703  ndmovass  6822  elovmpt2  6879  elovmpt2rab  6880  elovmpt2rab1  6881  elovmpt3rab1  6893  dfwe2  6981  opiota  7229  dfxp3  7230  bropopvvv  7255  oaord  7627  oeeu  7683  nnaord  7699  swoso  7775  fiint  8237  funsnfsupp  8299  alephval3  8933  fpwwe2lem8  9459  fpwwe2lem9  9460  fpwwe2lem12  9463  ingru  9637  axgroth3  9653  ltrelxr  10099  ltxrlt  10108  wloglei  10560  sup2  10979  rexuz2  11739  ltxr  11949  elixx3g  12188  ixxun  12191  elioo4g  12234  elioopnf  12267  elioomnf  12268  elicopnf  12269  elxrge0  12281  divelunit  12314  elfz2  12333  elfzuzb  12336  uzsplit  12412  fznn0  12432  elfzmlbp  12450  preduz  12461  elfzo2  12473  fzolb2  12477  fzouzsplit  12503  ssfzo12bi  12563  fzind2  12586  ccatsymb  13366  swrdsbslen  13448  swrdspsleq  13449  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccatin12lem3  13490  swrdccatin12  13491  repsdf2  13525  repswsymball  13526  repswsymballbi  13527  repswswrd  13531  s3eq3seq  13684  wrdl3s3  13705  s3sndisj  13706  s3iunsndisj  13707  abs2dif  14072  sinltx  14919  divalglem8  15123  divalglem10  15125  divalgb  15127  bitsval2  15147  divgcdz  15233  rplpwr  15276  cncongr1  15381  pythagtriplem2  15522  pythagtrip  15539  prmgaplem4  15758  setsstruct2  15896  pwsle  16152  imasvscafn  16197  mreexmrid  16303  iscatd2  16342  issect  16413  issect2  16414  oppcsect  16438  isfunc  16524  funcpropd  16560  fucsect  16632  fucinv  16633  initoeu2  16666  setcsect  16739  setcinv  16740  issubm2  17348  issubg3  17612  resgrpisgrp  17615  cycsubgcl  17620  eqgval  17643  eqger  17644  isgim  17704  gaorb  17740  gaorber  17741  gastacos  17743  symg2bas  17818  galactghm  17823  gsmsymgreqlem2  17851  pmtr3ncom  17895  ispgp  18007  efgcpbllema  18167  efgcpbllemb  18168  eqgabl  18240  dprdw  18409  ringpropd  18582  ringrghm  18605  isirred2  18701  rim0to0  18742  drngid2  18763  islss  18935  islmim  19062  lmhmpropd  19073  isassa  19315  mpfrcl  19518  zndvds  19898  znleval  19903  znleval2  19904  obselocv  20072  matinvgcell  20241  mat1dimscm  20281  scmatscm  20319  scmatf1  20337  mdetunilem7  20424  cpmatacl  20521  cpmatmcl  20524  mat2pmatf1  20534  mat2pmatghm  20535  mat2pmatmul  20536  mat2pmatlin  20540  mat2pmatscmxcl  20545  m2pmfzgsumcl  20553  decpmataa0  20573  monmatcollpw  20584  pmatcollpwscmatlem1  20594  pmatcollpwscmatlem2  20595  pm2mpghm  20621  pm2mpmhmlem2  20624  monmat2matmon  20629  chfacfisf  20659  chfacfisfcpmat  20660  chfacfpmmulgsum2  20670  isbasis3g  20753  leordtvallem2  21015  lmfval  21036  lmbr  21062  lmbr2  21063  lmmo  21184  dfconn2  21222  ptbasin  21380  ptbasfi  21384  txcnpi  21411  ptcnp  21425  hausdiag  21448  qtophmeo  21620  fbunfip  21673  elflim2  21768  hausflimi  21784  isfcls  21813  isfcls2  21817  istmd  21878  istgp  21881  istrg  21967  istdrg  21969  istdrg2  21981  istlm  21988  imasdsf1olem  22178  xmeterval  22237  xmeter  22238  prdsxmslem2  22334  blval2  22367  isngp  22400  isngp2  22401  isngp3  22402  isnlm  22479  cnbl0  22577  cnblcld  22578  elii1  22734  isphtpc  22793  phtpcer  22794  phtpcerOLD  22795  isclmp  22897  iscph  22970  lmmbr  23056  lmmbr2  23057  lmmbrf  23060  iscfil2  23064  iscau3  23076  iscau4  23077  iscauf  23078  caucfil  23081  isbn  23135  ishl2  23166  ovolfcl  23235  ioombl1lem4  23329  mbfmax  23416  iblpos  23559  limcrcl  23638  ig1pval3  23934  ulmdvlem3  24156  ellogdm  24385  relogbcl  24511  fsumvma2  24939  chpchtsum  24944  chpub  24945  dchrelbas3  24963  gausslemma2dlem1a  25090  lnhl  25510  colopp  25661  dfcgra2  25721  axeuclidlem  25842  axeuclid  25843  edgupgr  26029  umgr2edg1  26103  subusgr  26181  nb3grpr2  26285  nb3gr2nb  26286  isuvtxa  26295  nbupgruvtxres  26308  iscplgredg  26313  cplgr3v  26331  rusgrpropedg  26480  rgrusgrprc  26485  rusgrprc  26486  upgriswlk  26537  wlkonprop  26554  wksonproplem  26601  usgr2pth0  26661  isclwlke  26673  crctcshtrl  26715  iswwlksnx  26731  wwlknbp  26733  2trld  26834  rusgrnumwwlkl1  26863  rusgrnumwwlkb0  26866  rusgrnumwwlk  26870  erclwwlksref  26934  erclwwlksnref  26946  clwlksf1clwwlklem0  26964  0wlk  26977  3spthd  27036  umgr3v3e3cycl  27044  frgr3v  27139  1to3vfriswmgr  27144  frgr2wwlkeu  27191  numclwwlkovfel2  27216  numclwwlkovf2  27217  numclwlk1lem2fo  27228  nvex  27466  isnv  27467  dfadj2  28744  cnvadj  28751  adjeq  28794  eleigvec  28816  eleigvec2  28817  chirredi  29253  or3di  29307  dfrp2  29532  eliccelico  29539  omndmul2  29712  isorng  29799  pmtrprfv2  29848  fzto1st  29853  psgnfzto1st  29855  eulerpartlemv  30426  eulerpartlemd  30428  eulerpartlemn  30443  prob01  30475  probun  30481  bnj170  30764  bnj248  30766  bnj252  30769  bnj253  30770  bnj945  30844  bnj1098  30854  bnj1224  30872  bnj150  30946  bnj153  30950  bnj545  30965  bnj557  30971  bnj571  30976  bnj594  30982  bnj864  30992  bnj865  30993  bnj849  30995  bnj964  31013  bnj986  31024  bnj996  31025  bnj1033  31037  bnj1110  31050  bnj1128  31058  bnj1174  31071  pconnconn  31213  resconn  31228  iscvm  31241  cvmlift2lem12  31296  cvmlift3lem5  31305  elmpst  31433  mpstrcl  31438  lediv2aALT  31571  dfso3  31601  br6  31647  etasslt  31920  elfuns  32022  brimg  32044  brsuccf  32048  cgrxfr  32162  segcon2  32212  seglecgr12im  32217  seglecgr12  32218  segletr  32221  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsidele  32239  bj-imn3ani  32572  relowlpssretop  33212  lindsenlbs  33404  matunitlindflem2  33406  fdc  33541  isbnd3b  33584  ablo4pnp  33679  crngm4  33802  isidlc  33814  pridl  33836  ispridl2  33837  ispridlc  33869  ts3an1  33957  ts3an2  33958  ts3an3  33959  brres2  34035  eldmqsres  34051  islshpsm  34267  islshpat  34304  cmtfvalN  34497  cmtvalN  34498  ishlat1  34639  ishlat2  34640  3dim0  34743  2dim  34756  islvol5  34865  lhpexle3  35298  cdleme0ex2N  35511  cdleme0nex  35577  cdlemg2cex  35879  cdlemg33b0  35989  cdlemg33b  35995  cdlemg33c  35996  cdlemg33e  35998  dib1dim  36454  diblsmopel  36460  dihopelvalcpre  36537  lcfls1c  36825  3anrabdioph  37346  issdrg2  37768  fgraphxp  37789  dfrtrcl5  37936  brfvrcld2  37984  df3an2  38061  dfvd3  38807  3impexpVD  39091  rfcnnnub  39195  stoweidlem35  40252  smflimlem4  40982  ndmaovass  41286  nltle2tri  41323  elfz2z  41325  pfxccatin12lem2  41424  pfxccatin12  41425  pfxccat3a  41429  gboge9  41652  sbgoldbalt  41669  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  bgoldbtbndlem4  41696  bgoldbtbnd  41697  ismhm0  41805  rnglz  41884  rngcsect  41980  rngcinv  41981  rngcsectALTV  41992  rngcinvALTV  41993  ringcsect  42031  ringcinv  42032  ringcsectALTV  42055  ringcinvALTV  42056  islindeps  42242  islindeps2  42272  isldepslvec2  42274  elbigo2  42346