Definition df-3an 1011

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 405. (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 1009	. 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 used by:  3anass  1013  3anrot  1014  3ancoma  1016  3anan32  1020  3ioran  1024  3simpa  1025  3pm3.2i  1206  pm3.2an3  1207  3jca  1208  3anbi123i  1219  3imp  1224  3anbi123d  1353  3anim123d  1360  an6  1362  19.26-3an  1536  hb3an  1603  nf3an  1619  nf3and  1622  eeeanv  1993  sb3an  2018  mopick2  2170  r19.26-3  2681  3reeanv  2722  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  sbc3an  3113  elin3  3420  rexdifpr  3737  raltpg  3762  tpss  3883  dfopg  3902  opeq1  3904  opeq2  3905  opm  4374  otth2  4381  poirr  4452  po3nr  4455  wepo  4504  wetrep  4505  rabxp  4812  brinxp2  4842  brinxp  4843  sotri2  5185  sotri3  5186  f1orn  5649  dff1o6  5982  isosolem  6030  oprabid  6117  caovimo  6283  elovmpo  6288  elovmporab  6289  elovmporab1w  6290  dfxp3  6430  nnaord  6782  fiintim  7238  prmuloc  7933  ltrelxr  8386  rexuz2  9981  ltxr  10177  elixx3g  10303  elioo4g  10336  elioopnf  10369  elioomnf  10370  elicopnf  10371  elxrge0  10380  divelunit  10404  elfz2  10418  elfzuzb  10422  uzsplit  10499  fznn0  10520  elfzmlbp  10539  elfzo2  10557  fzolb2  10562  fzouzsplit  10588  ssfzo12bi  10643  fzind2  10658  dfrp2  10698  ccatsymb  11370  swrdsbslen  11438  swrdspsleq  11439  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3a  11510  abs2dif  11872  sumeq2  12125  divalgb  12692  bitsval2  12711  divgcdz  12748  rplpwr  12804  nnwosdc  12816  cncongr1  12881  pythagtriplem2  13045  pythagtrip  13062  ballotfilemelo  13222  xpscf  13668  issgrpd  13727  issubm2  13780  issubg3  13995  resgrpisgrp  13998  eqgval  14026  eqger  14027  eqgabl  14134  qusecsub  14135  rnglz  14244  rngpropd  14254  ringpropd  14343  ringrghm  14367  zndvds  14984  znleval  14988  znleval2  14989  isbasis3g  15147  lmfval  15294  lmbr  15314  lmbr2  15315  xmeterval  15536  xmeter  15537  cnbl0  15635  cnblcld  15636  limcrcl  15759  gausslemma2dlem1a  16177  umgr2edg1  16450  subusgr  16516  upgriswlkdc  16601  clwwlknon2x  16676  bd3an  16856