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  1494  hb3an  1561  nf3an  1577  nf3and  1580  eeeanv  1949  sb3an  1974  mopick2  2125  r19.26-3  2624  3reeanv  2665  ceqsex3v  2802  ceqsex4v  2803  ceqsex8v  2805  sbc3an  3047  elin3  3350  rexdifpr  3646  raltpg  3671  tpss  3784  dfopg  3802  opeq1  3804  opeq2  3805  opm  4263  otth2  4270  poirr  4338  po3nr  4341  wepo  4390  wetrep  4391  rabxp  4696  brinxp2  4726  brinxp  4727  sotri2  5063  sotri3  5064  f1orn  5510  dff1o6  5819  isosolem  5867  oprabid  5950  caovimo  6112  elovmpo  6117  elovmporab  6118  elovmporab1w  6119  dfxp3  6247  nnaord  6562  fiintim  6985  prmuloc  7626  ltrelxr  8080  rexuz2  9646  ltxr  9841  elixx3g  9967  elioo4g  10000  elioopnf  10033  elioomnf  10034  elicopnf  10035  elxrge0  10044  divelunit  10068  elfz2  10081  elfzuzb  10085  uzsplit  10158  fznn0  10179  elfzmlbp  10198  elfzo2  10216  fzolb2  10221  fzouzsplit  10246  ssfzo12bi  10292  fzind2  10306  dfrp2  10332  abs2dif  11250  sumeq2  11502  divalgb  12066  divgcdz  12108  rplpwr  12164  nnwosdc  12176  cncongr1  12241  pythagtriplem2  12404  pythagtrip  12421  xpscf  12930  issgrpd  12995  issubm2  13045  issubg3  13262  resgrpisgrp  13265  eqgval  13293  eqger  13294  eqgabl  13400  qusecsub  13401  rnglz  13441  rngpropd  13451  ringpropd  13534  ringrghm  13558  zndvds  14137  znleval  14141  znleval2  14142  isbasis3g  14214  lmfval  14360  lmbr  14381  lmbr2  14382  xmeterval  14603  xmeter  14604  cnbl0  14702  cnblcld  14703  limcrcl  14812  gausslemma2dlem1a  15174  bd3an  15322