Definition df-3an 1007

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 1005	. 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  1009  3anrot  1010  3ancoma  1012  3anan32  1016  3ioran  1020  3simpa  1021  3pm3.2i  1202  pm3.2an3  1203  3jca  1204  3anbi123i  1215  3imp  1220  3anbi123d  1349  3anim123d  1356  an6  1358  19.26-3an  1532  hb3an  1599  nf3an  1615  nf3and  1618  eeeanv  1989  sb3an  2014  mopick2  2166  r19.26-3  2675  3reeanv  2716  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  sbc3an  3107  elin3  3414  rexdifpr  3722  raltpg  3747  tpss  3867  dfopg  3886  opeq1  3888  opeq2  3889  opm  4355  otth2  4362  poirr  4433  po3nr  4436  wepo  4485  wetrep  4486  rabxp  4792  brinxp2  4822  brinxp  4823  sotri2  5165  sotri3  5166  f1orn  5629  dff1o6  5955  isosolem  6003  oprabid  6090  caovimo  6256  elovmpo  6261  elovmporab  6262  elovmporab1w  6263  dfxp3  6403  nnaord  6755  fiintim  7204  prmuloc  7897  ltrelxr  8350  rexuz2  9934  ltxr  10130  elixx3g  10256  elioo4g  10289  elioopnf  10322  elioomnf  10323  elicopnf  10324  elxrge0  10333  divelunit  10357  elfz2  10371  elfzuzb  10375  uzsplit  10451  fznn0  10472  elfzmlbp  10491  elfzo2  10509  fzolb2  10514  fzouzsplit  10540  ssfzo12bi  10595  fzind2  10610  dfrp2  10650  ccatsymb  11318  swrdsbslen  11386  swrdspsleq  11387  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccatin12  11453  pfxccat3a  11458  abs2dif  11820  sumeq2  12073  divalgb  12640  bitsval2  12659  divgcdz  12696  rplpwr  12752  nnwosdc  12764  cncongr1  12829  pythagtriplem2  12993  pythagtrip  13010  ballotfilemelo  13170  xpscf  13615  issgrpd  13679  issubm2  13732  issubg3  13949  resgrpisgrp  13952  eqgval  13980  eqger  13981  eqgabl  14087  qusecsub  14088  rnglz  14188  rngpropd  14198  ringpropd  14285  ringrghm  14309  zndvds  14927  znleval  14931  znleval2  14932  isbasis3g  15041  lmfval  15188  lmbr  15208  lmbr2  15209  xmeterval  15430  xmeter  15431  cnbl0  15529  cnblcld  15530  limcrcl  15653  gausslemma2dlem1a  16061  umgr2edg1  16334  subusgr  16400  upgriswlkdc  16485  clwwlknon2x  16560  bd3an  16740