Definition df-3an 982

Description: Define conjunction ('and') of 3 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 401. (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 980	. 2 wff ( ph /\ ps /\ ch )
5	1, 2	wa 104	. . 3 wff ( ph /\ ps )
6	5, 3	wa 104	. 2 wff ( ( ph /\ ps ) /\ ch )
7	4, 6	wb 105	1 wff ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

This definition is referenced by:  3anass  984  3anrot  985  3ancoma  987  3anan32  991  3ioran  995  3simpa  996  3pm3.2i  1177  pm3.2an3  1178  3jca  1179  3anbi123i  1190  3imp  1195  3anbi123d  1323  3anim123d  1330  an6  1332  19.26-3an  1497  hb3an  1564  nf3an  1580  nf3and  1583  eeeanv  1952  sb3an  1977  mopick2  2128  r19.26-3  2627  3reeanv  2668  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  sbc3an  3051  elin3  3355  rexdifpr  3651  raltpg  3676  tpss  3789  dfopg  3807  opeq1  3809  opeq2  3810  opm  4268  otth2  4275  poirr  4343  po3nr  4346  wepo  4395  wetrep  4396  rabxp  4701  brinxp2  4731  brinxp  4732  sotri2  5068  sotri3  5069  f1orn  5517  dff1o6  5826  isosolem  5874  oprabid  5957  caovimo  6121  elovmpo  6126  elovmporab  6127  elovmporab1w  6128  dfxp3  6261  nnaord  6576  fiintim  7001  prmuloc  7650  ltrelxr  8104  rexuz2  9672  ltxr  9867  elixx3g  9993  elioo4g  10026  elioopnf  10059  elioomnf  10060  elicopnf  10061  elxrge0  10070  divelunit  10094  elfz2  10107  elfzuzb  10111  uzsplit  10184  fznn0  10205  elfzmlbp  10224  elfzo2  10242  fzolb2  10247  fzouzsplit  10272  ssfzo12bi  10318  fzind2  10332  dfrp2  10370  abs2dif  11288  sumeq2  11541  divalgb  12107  bitsval2  12126  divgcdz  12163  rplpwr  12219  nnwosdc  12231  cncongr1  12296  pythagtriplem2  12460  pythagtrip  12477  xpscf  13049  issgrpd  13114  issubm2  13175  issubg3  13398  resgrpisgrp  13401  eqgval  13429  eqger  13430  eqgabl  13536  qusecsub  13537  rnglz  13577  rngpropd  13587  ringpropd  13670  ringrghm  13694  zndvds  14281  znleval  14285  znleval2  14286  isbasis3g  14366  lmfval  14512  lmbr  14533  lmbr2  14534  xmeterval  14755  xmeter  14756  cnbl0  14854  cnblcld  14855  limcrcl  14978  gausslemma2dlem1a  15383  bd3an  15560