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  5582  dff1o6  5900  isosolem  5948  oprabid  6033  caovimo  6199  elovmpo  6204  elovmporab  6205  elovmporab1w  6206  dfxp3  6340  nnaord  6655  fiintim  7093  prmuloc  7753  ltrelxr  8207  rexuz2  9776  ltxr  9971  elixx3g  10097  elioo4g  10130  elioopnf  10163  elioomnf  10164  elicopnf  10165  elxrge0  10174  divelunit  10198  elfz2  10211  elfzuzb  10215  uzsplit  10288  fznn0  10309  elfzmlbp  10328  elfzo2  10346  fzolb2  10351  fzouzsplit  10377  ssfzo12bi  10431  fzind2  10445  dfrp2  10483  ccatsymb  11137  swrdsbslen  11198  swrdspsleq  11199  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3a  11270  abs2dif  11617  sumeq2  11870  divalgb  12436  bitsval2  12455  divgcdz  12492  rplpwr  12548  nnwosdc  12560  cncongr1  12625  pythagtriplem2  12789  pythagtrip  12806  xpscf  13380  issgrpd  13445  issubm2  13506  issubg3  13729  resgrpisgrp  13732  eqgval  13760  eqger  13761  eqgabl  13867  qusecsub  13868  rnglz  13908  rngpropd  13918  ringpropd  14001  ringrghm  14025  zndvds  14613  znleval  14617  znleval2  14618  isbasis3g  14720  lmfval  14867  lmbr  14887  lmbr2  14888  xmeterval  15109  xmeter  15110  cnbl0  15208  cnblcld  15209  limcrcl  15332  gausslemma2dlem1a  15737  umgr2edg1  16007  upgriswlkdc  16071  bd3an  16193