MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3an Unicode version

Definition df-3an 941
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. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3an  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3w3a 939 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 360 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 360 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 178 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  943  3anrot  944  3ancoma  946  3anan32  951  3anor  953  3ioran  955  3simpa  957  3pm3.2i  1135  pm3.2an3  1136  3jca  1137  3anbi123i  1145  3imp  1150  3anbi123d  1257  3anim123d  1264  an6  1266  cadan  1388  19.26-3an  1594  hb3an  1725  nf3and  1730  nf3an  1740  sb3an  1963  eeeanv  2059  mopick2  2183  r19.26-3  2650  3reeanv  2681  ceqsex3v  2794  ceqsex4v  2795  ceqsex8v  2797  elin3  3321  raltpg  3644  tpss  3739  dfopif  3753  disjxun  3981  otth2  4207  oteqex  4217  poirr  4283  po3nr  4286  wefrc  4345  dfwe2  4531  rabxp  4699  brinxp2  4725  brinxp  4726  f1orn  5406  dff1o6  5711  oprabid  5802  ndmovass  5928  elovmpt2  5984  dfxp3  6099  opiota  6242  oaord  6499  oeeui  6554  oeeu  6555  nnaord  6571  swoso  6645  fiint  7087  alephval3  7691  fpwwe2lem8  8213  fpwwe2lem9  8214  fpwwe2lem12  8217  ingru  8391  axgroth3  8407  ltrelxr  8840  ltxrlt  8847  wloglei  9259  sup2  9664  rexuz2  10223  ltxr  10410  elixx3g  10621  ixxun  10624  elioo4g  10663  elioopnf  10689  elioomnf  10690  elicopnf  10691  elxrge0  10699  elfz2  10741  elfzuzb  10744  fznn0  10803  uzsplit  10807  elfzo2  10830  fzolb2  10833  fzouzsplit  10853  fzind2  10875  abs2dif  11767  sinltx  12417  divalglem8  12547  divalglem10  12549  divalgb  12551  bitsval2  12564  rplpwr  12683  pythagtriplem2  12818  pythagtrip  12835  pwsle  13339  imasvscafn  13387  mreexmrid  13493  iscatd2  13531  issect  13604  issect2  13605  oppcsect  13624  isfunc  13686  funcpropd  13722  fucsect  13794  fucinv  13795  setcsect  13869  setcinv  13870  mndcl  14320  issubm2  14374  issubg3  14585  cycsubgcl  14591  eqgval  14614  eqger  14615  isgim  14674  gaorb  14709  gaorber  14710  gastacos  14712  galactghm  14731  ispgp  14851  efgcpbllema  15011  efgcpbllemb  15012  eqgabl  15079  dprdw  15193  rngpropd  15320  rngrghm  15337  isirred2  15431  drngid2  15476  islss  15640  islmim  15763  lmhmpropd  15774  isassa  16004  zndvds  16451  znleval  16456  znleval2  16457  obselocv  16576  isbasis3g  16635  leordtvallem2  16889  lmfval  16910  lmbr  16936  lmbr2  16937  lmmo  17056  dfcon2  17093  ptbasin  17220  ptbasfi  17224  txcnpi  17250  ptcnp  17264  hausdiag  17287  qtophmeo  17456  fbunfip  17512  elflim2  17607  hausflimi  17623  isfcls  17652  isfcls2  17656  istmd  17705  istgp  17708  istrg  17794  istdrg  17796  istdrg2  17808  istlm  17815  imasdsf1olem  17885  xmeterval  17926  xmeter  17927  prdsxmslem2  18023  isngp  18066  isngp2  18067  isngp3  18068  isnlm  18134  cnbl0  18231  cnblcld  18232  elii1  18381  isphtpc  18440  phtpcer  18441  iscph  18554  lmmbr  18632  lmmbr2  18633  lmmbrf  18636  iscfil2  18640  iscau3  18652  iscau4  18653  iscauf  18654  caucfil  18657  isbn  18708  ishl2  18735  ovolfcl  18774  ioombl1lem4  18866  mbfmax  18952  iblpos  19095  limcrcl  19172  mpfrcl  19350  ig1pval3  19508  ulmdvlem3  19727  ellogdm  19934  fsumvma2  20401  chpchtsum  20406  chpub  20407  dchrelbas3  20425  nvex  21113  isnv  21114  dfadj2  22411  cnvadj  22418  adjeq  22461  eleigvec  22483  eleigvec2  22484  chirredi  22920  ballotlem2  22994  pconcon  23120  rescon  23135  iscvm  23148  cvmlift2lem12  23203  cvmlift3lem5  23212  lediv2aALT  23371  dfso3  23432  divelunit  23437  br6  23471  preduz  23555  axfelem9  23709  brsuccf  23841  axeuclidlem  23951  axeuclid  23952  cgrxfr  24039  segcon2  24089  seglecgr12im  24094  seglecgr12  24095  segletr  24098  btwnoutside  24109  broutsideof3  24110  outsideoftr  24113  outsidele  24116  eqvinopb  24317  copsexgb  24318  elo  24393  dff1o6f  24444  prismorcsetlem  25265  prismorcset  25267  prismorcsetlemc  25270  cmppar  25326  cmppar3  25327  isibcg  25544  fdc  25808  isbnd3b  25862  ablo4pnp  25923  crngm4  25981  isidlc  25993  pridl  26015  ispridl2  26016  ispridlc  26048  3anrabdioph  26215  issdrg2  26859  fgraphxp  26883  rfcnnnub  27061  stoweidlem35  27105  dfvd3  27397  3impexpVD  27666  bnj170  27756  bnj248  27758  bnj252  27761  bnj253  27762  bnj945  27838  bnj1098  27848  bnj1224  27867  bnj150  27941  bnj153  27945  bnj545  27960  bnj557  27966  bnj571  27971  bnj594  27977  bnj864  27987  bnj865  27988  bnj849  27990  bnj964  28008  bnj986  28019  bnj996  28020  bnj1033  28032  bnj1110  28045  bnj1128  28053  bnj1174  28066  islshpsm  28321  islshpat  28358  cmtfvalN  28551  cmtvalN  28552  ishlat1  28693  ishlat2  28694  3dim0  28797  2dim  28810  islvol5  28919  lhpexle3  29352  cdleme0ex2N  29564  cdleme0nex  29630  cdlemg2cex  29931  cdlemg33b0  30041  cdlemg33b  30047  cdlemg33c  30048  cdlemg33e  30050  dib1dim  30506  diblsmopel  30512  dihopelvalcpre  30589  lcfls1c  30877
  Copyright terms: Public domain W3C validator