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

Definition df-3an 938
Description: Define conjunction ('and') of three 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 631. (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 936 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 359 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 359 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 177 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  940  3anrot  941  3ancoma  943  3anan32  948  3anor  950  3ioran  952  3simpa  954  3pm3.2i  1132  pm3.2an3  1133  3jca  1134  3anbi123i  1142  3imp  1147  3anbi123d  1254  3anim123d  1261  an6  1263  cadan  1401  19.26-3an  1605  nf3and  1844  nf3an  1849  hb3anOLD  1853  4exdistr  1934  eeeanv  1938  eeeanvOLD  1939  sb3an  2140  mopick2  2348  r19.26-3  2840  3reeanv  2876  ceqsex3v  2994  ceqsex4v  2995  ceqsex8v  2997  elin3  3532  raltpg  3859  tpss  3964  dfopif  3981  disjxun  4210  otth2  4439  oteqex  4449  poirr  4514  po3nr  4517  wefrc  4576  dfwe2  4762  rabxp  4914  brinxp2  4939  brinxp  4940  f1orn  5684  dff1o6  6013  oprabid  6105  ndmovass  6235  elovmpt2  6291  dfxp3  6406  bropopvvv  6426  opiota  6535  oaord  6790  oeeui  6845  oeeu  6846  nnaord  6862  swoso  6936  fiint  7383  alephval3  7991  fpwwe2lem8  8512  fpwwe2lem9  8513  fpwwe2lem12  8516  ingru  8690  axgroth3  8706  ltrelxr  9139  ltxrlt  9146  wloglei  9559  sup2  9964  rexuz2  10528  ltxr  10715  elixx3g  10929  ixxun  10932  elioo4g  10971  elioopnf  10998  elioomnf  10999  elicopnf  11000  elxrge0  11008  elfz2  11050  elfzuzb  11053  fznn0  11113  uzsplit  11118  elfzo2  11143  fzolb2  11146  fzouzsplit  11168  fzind2  11198  abs2dif  12136  sinltx  12790  divalglem8  12920  divalglem10  12922  divalgb  12924  bitsval2  12937  rplpwr  13056  pythagtriplem2  13191  pythagtrip  13208  pwsle  13714  imasvscafn  13762  mreexmrid  13868  iscatd2  13906  issect  13979  issect2  13980  oppcsect  13999  isfunc  14061  funcpropd  14097  fucsect  14169  fucinv  14170  setcsect  14244  setcinv  14245  mndcl  14695  issubm2  14749  issubg3  14960  cycsubgcl  14966  eqgval  14989  eqger  14990  isgim  15049  gaorb  15084  gaorber  15085  gastacos  15087  galactghm  15106  ispgp  15226  efgcpbllema  15386  efgcpbllemb  15387  eqgabl  15454  dprdw  15568  rngpropd  15695  rngrghm  15712  isirred2  15806  drngid2  15851  islss  16011  islmim  16134  lmhmpropd  16145  isassa  16375  zndvds  16830  znleval  16835  znleval2  16836  obselocv  16955  isbasis3g  17014  leordtvallem2  17275  lmfval  17296  lmbr  17322  lmbr2  17323  lmmo  17444  dfcon2  17482  ptbasin  17609  ptbasfi  17613  txcnpi  17640  ptcnp  17654  hausdiag  17677  qtophmeo  17849  fbunfip  17901  elflim2  17996  hausflimi  18012  isfcls  18041  isfcls2  18045  istmd  18104  istgp  18107  istrg  18193  istdrg  18195  istdrg2  18207  istlm  18214  imasdsf1olem  18403  xmeterval  18462  xmeter  18463  prdsxmslem2  18559  blval2  18605  isngp  18643  isngp2  18644  isngp3  18645  isnlm  18711  cnbl0  18808  cnblcld  18809  elii1  18960  isphtpc  19019  phtpcer  19020  iscph  19133  lmmbr  19211  lmmbr2  19212  lmmbrf  19215  iscfil2  19219  iscau3  19231  iscau4  19232  iscauf  19233  caucfil  19236  isbn  19291  ishl2  19324  ovolfcl  19363  ioombl1lem4  19455  mbfmax  19541  iblpos  19684  limcrcl  19761  mpfrcl  19939  ig1pval3  20097  ulmdvlem3  20318  ellogdm  20530  fsumvma2  20998  chpchtsum  21003  chpub  21004  dchrelbas3  21022  nb3grapr2  21463  nb3gra2nb  21464  0wlk  21545  0trl  21546  constr2wlk  21598  3v3e3cycl1  21631  nvex  22090  isnv  22091  dfadj2  23388  cnvadj  23395  adjeq  23438  eleigvec  23460  eleigvec2  23461  chirredi  23897  or3di  23951  eliccelico  24140  relogbcl  24402  prob01  24671  probun  24677  pconcon  24918  rescon  24933  iscvm  24946  cvmlift2lem12  25001  cvmlift3lem5  25010  lediv2aALT  25117  dfso3  25177  divelunit  25185  br6  25380  preduz  25475  nofulllem2  25658  nofulllem5  25661  elfuns  25760  brimg  25782  brsuccf  25786  axeuclidlem  25901  axeuclid  25902  cgrxfr  25989  segcon2  26039  seglecgr12im  26044  seglecgr12  26045  segletr  26048  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  outsidele  26066  fdc  26449  isbnd3b  26494  ablo4pnp  26555  crngm4  26613  isidlc  26625  pridl  26647  ispridl2  26648  ispridlc  26680  3anrabdioph  26841  issdrg2  27483  fgraphxp  27507  rfcnnnub  27683  stoweidlem35  27760  ndmaovass  28046  3an4anass  28049  rexdifpr  28059  otthg  28064  oprabv  28085  elfz2z  28105  elfzmlbp  28107  ccatsymb  28179  swrdccatin2  28210  swrdccatin12lem3  28212  swrdccatin12lem4  28213  swrdccatin12  28214  cshweqdif2s  28271  usgra2pth0  28312  el2wlkonotot0  28339  el2wlkonotot  28340  el2wlkonotot1  28341  2wlkonotv  28344  usg2spthonot0  28356  cusgraisrusgra  28377  frgra3v  28392  1to3vfriswmgra  28397  ex3  28658  dfvd3  28683  3impexpVD  28968  bnj170  29062  bnj248  29064  bnj252  29067  bnj253  29068  bnj945  29144  bnj1098  29154  bnj1224  29173  bnj150  29247  bnj153  29251  bnj545  29266  bnj557  29272  bnj571  29277  bnj594  29283  bnj864  29293  bnj865  29294  bnj849  29296  bnj964  29314  bnj986  29325  bnj996  29326  bnj1033  29338  bnj1110  29351  bnj1128  29359  bnj1174  29372  sb3anNEW7  29640  eeeanvOLD7  29704  islshpsm  29778  islshpat  29815  cmtfvalN  30008  cmtvalN  30009  ishlat1  30150  ishlat2  30151  3dim0  30254  2dim  30267  islvol5  30376  lhpexle3  30809  cdleme0ex2N  31021  cdleme0nex  31087  cdlemg2cex  31388  cdlemg33b0  31498  cdlemg33b  31504  cdlemg33c  31505  cdlemg33e  31507  dib1dim  31963  diblsmopel  31969  dihopelvalcpre  32046  lcfls1c  32334
  Copyright terms: Public domain W3C validator