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  9990  ltxr  10187  elixx3g  10313  elioo4g  10346  elioopnf  10379  elioomnf  10380  elicopnf  10381  elxrge0  10390  divelunit  10414  elfz2  10428  elfzuzb  10432  uzsplit  10509  fznn0  10530  elfzmlbp  10549  elfzo2  10567  fzolb2  10572  fzouzsplit  10598  ssfzo12bi  10653  fzind2  10668  dfrp2  10708  ccatsymb  11384  swrdsbslen  11452  swrdspsleq  11453  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3a  11524  abs2dif  11887  sumeq2  12141  divalgb  12708  bitsval2  12727  divgcdz  12764  rplpwr  12820  nnwosdc  12832  cncongr1  12897  pythagtriplem2  13065  pythagtrip  13082  ballotfilemelo  13271  xpscf  13717  issgrpd  13776  issubm2  13829  issubg3  14044  resgrpisgrp  14047  eqgval  14075  eqger  14076  eqgabl  14183  qusecsub  14184  rnglz  14293  rngpropd  14303  ringpropd  14392  ringrghm  14416  zndvds  15033  znleval  15037  znleval2  15038  isbasis3g  15196  lmfval  15343  lmbr  15363  lmbr2  15364  xmeterval  15585  xmeter  15586  cnbl0  15684  cnblcld  15685  limcrcl  15808  gausslemma2dlem1a  16275  umgr2edg1  16548  subusgr  16614  upgriswlkdc  16699  clwwlknon2x  16774  bd3an  16954