Definition df-3an 1104

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 633.

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 1102	. 2 wff (ph /\ ps /\ ch)
5	1, 2	wa 337	. . 3 wff (ph /\ ps)
6	5, 3	wa 337	. 2 wff ((ph /\ ps) /\ ch)
7	4, 6	wb 219	1 wff ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))

This definition is referenced by:  3anass 1106  3anrot 1107  3ancoma 1109  3anor 1113  3ioran 1115  3simpa 1117  3pm3.2i 1298  pm3.2an3 1299  3jca 1300  3anbi123i 1306  3imp 1311  3anbi123d 1441  3anim123d 1448  an6 1450  hb3an 1648  19.26-3an 1705  sb3an 1884  eeeanv 1975  mopick2 2099  3reeanv 2494  ceqsex3v 2575  ceqsex4v 2576  ceqsex8v 2578  tpss 3334  otthg 3698  poirr 3757  po3nr 3760  pofun 3763  wefrc 3806  dfwe2 4007  brinxp 4191  dff1o3 4728  f1orn 4732  dff1o6 4948  oprabid 5002  ndmoprass 5074  tz7.49cOLD 5334  tz7.49c 5336  oaord 5392  fiint 5872  abfii2 5874  alephval3 6233  sup2 7600  elioo3g 7893  eliooord 7902  rexuz2 7961  elfz2 8003  elfzuzb 8007  fznn0 8057  fznn 8058  expword2i 8234  abs2dif 8539  climcmplem 8793  isumcmpii 8872  mulc1cncf 8939  infxpidmlem7OLD 9221  divalglem8 9297  divalglem10 9299  divalgb 9301  exprmfctlem 9380  isbasis3g 9733  bl2in 9986  lmfval 10069  iscauf 10083  iscau5 10085  iscaunns 10088  nvex 10431  isnv 10432  sspval 10590  efifolem4 10950  axgroth3 11009  symgoprab 11033  hmph 11076  fbunfip 11120  flimff 11155  h2hcau 11319  dfadj2 12281  cnvadj 12285  adjeq 12328  eleigvec2 12351  irredi 12797  bnj169 12864  bnj170 12865  bnj171 12866  bnj172 12867  bnj173 12868  bnj178 12873  bnj248 12907  bnj252 12911  bnj253 12912  bnj180 13274  bnj512 13292  bnj574 13318  bnj856 13560  bnj861 13565  bnj945 13615  bnj962 13627  bnj980 13633  bnj1111 13695  bnj1224 13770  bnj109 13997  bnj129 14010  bnj149 14012  bnj153 14018  bnj557 14052  bnj571 14060  bnj849 14089  bnj986 14131  bnj996 14133  bnj1128 14199  bnj1174 14213  lediv2aALT 14413  elno3 14661  axfelem9 14707  ellimits 14771  r19.26t 14982  dff1o6f 15128  oprabval2gc 15188  oprabval4gc 15189  iscst1 15258  iscst2 15259  dmhmph 15643  rnhmph 15644  hmeogrp 15649  efilcp 15688  efilcp2 15692  cnfilca 15693  limfillem1 15704  grphmlem2 15770  grphlem3 15771  grphm 15774  ishoma 15930  ishomb 15931  isseg1 16114  isseg2 16115  compfipin0 16260  dfcon2 16266  fbasfip 16380  filssufillem 16394  fclsfnflim 16438  flimfnfcls 16439  fclusff 16447  3reeanvOLD 16485  pofunOLD 16596  fdc 16636  abl4pnp 16861  phtpcer 16886  pcoval 16897  pcoloopf 16903  crngm4 16975  isidlc 16987  pridl 17009  ispridl2 17010  ispridlc 17042  dfvd3 17325  3impexpVD 17514  cmtfval 17604  cmtval 17605  ishlat1 17748  ishlat2 17749  3dim0 17853  2dim 17866  islvol5 18011  cdleme0ex2 18593  cdleme0nex 18661  cdlemg2cex 18969

Copyright terms: Public domain