Definition df-3an 1004

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 1002	. 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  1006  3anrot  1007  3ancoma  1009  3anan32  1013  3ioran  1017  3simpa  1018  3pm3.2i  1199  pm3.2an3  1200  3jca  1201  3anbi123i  1212  3imp  1217  3anbi123d  1346  3anim123d  1353  an6  1355  19.26-3an  1529  hb3an  1596  nf3an  1612  nf3and  1615  eeeanv  1984  sb3an  2009  mopick2  2161  r19.26-3  2661  3reeanv  2702  ceqsex3v  2843  ceqsex4v  2844  ceqsex8v  2846  sbc3an  3090  elin3  3395  rexdifpr  3694  raltpg  3719  tpss  3836  dfopg  3855  opeq1  3857  opeq2  3858  opm  4320  otth2  4327  poirr  4398  po3nr  4401  wepo  4450  wetrep  4451  rabxp  4756  brinxp2  4786  brinxp  4787  sotri2  5126  sotri3  5127  f1orn  5584  dff1o6  5906  isosolem  5954  oprabid  6039  caovimo  6205  elovmpo  6210  elovmporab  6211  elovmporab1w  6212  dfxp3  6346  nnaord  6663  fiintim  7104  prmuloc  7764  ltrelxr  8218  rexuz2  9788  ltxr  9983  elixx3g  10109  elioo4g  10142  elioopnf  10175  elioomnf  10176  elicopnf  10177  elxrge0  10186  divelunit  10210  elfz2  10223  elfzuzb  10227  uzsplit  10300  fznn0  10321  elfzmlbp  10340  elfzo2  10358  fzolb2  10363  fzouzsplit  10389  ssfzo12bi  10443  fzind2  10457  dfrp2  10495  ccatsymb  11150  swrdsbslen  11214  swrdspsleq  11215  swrdccatin2  11277  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatin12  11281  pfxccat3a  11286  abs2dif  11633  sumeq2  11886  divalgb  12452  bitsval2  12471  divgcdz  12508  rplpwr  12564  nnwosdc  12576  cncongr1  12641  pythagtriplem2  12805  pythagtrip  12822  xpscf  13396  issgrpd  13461  issubm2  13522  issubg3  13745  resgrpisgrp  13748  eqgval  13776  eqger  13777  eqgabl  13883  qusecsub  13884  rnglz  13924  rngpropd  13934  ringpropd  14017  ringrghm  14041  zndvds  14629  znleval  14633  znleval2  14634  isbasis3g  14736  lmfval  14883  lmbr  14903  lmbr2  14904  xmeterval  15125  xmeter  15126  cnbl0  15224  cnblcld  15225  limcrcl  15348  gausslemma2dlem1a  15753  umgr2edg1  16023  upgriswlkdc  16106  bd3an  16276