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

Definition df-3an 1056
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 682. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3an ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3w3a 1054 . 2 wff (𝜑𝜓𝜒)
51, 2wa 383 . . 3 wff (𝜑𝜓)
65, 3wa 383 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 196 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1059  3anrot  1060  3ancoma  1062  3anan32  1068  3anorOLD  1072  3ioran  1073  3ianor  1074  3simpa  1078  3pm3.2i  1259  pm3.2an3  1260  3jca  1261  3anbi123i  1270  3imp  1275  3an4anass  1314  3anbi123d  1439  3anim123d  1446  an6  1448  an3andi  1485  an33rean  1486  cadan  1588  19.26-3an  1840  nf3and  1867  nf3an  1871  4exdistr  1927  eeeanv  2219  nf3andOLD  2269  nf3anOLD  2275  sb3an  2428  mopick2  2569  r3al  2969  r19.26-3  3095  3reeanv  3137  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  sbc3an  3527  elin3  3837  rexdifpr  4238  raltpg  4268  tpss  4400  dfopif  4430  disjxun  4683  otth2  4981  otthg  4983  oteqex  4993  poirr  5075  po3nr  5078  wefrc  5137  rabxp  5188  brinxp2  5214  brinxp  5215  f1orn  6185  fpropnf1  6564  dff1o6  6571  oprabid  6717  oprabv  6745  ndmovass  6864  elovmpt2  6921  elovmpt2rab  6922  elovmpt2rab1  6923  elovmpt3rab1  6935  dfwe2  7023  opiota  7273  dfxp3  7275  bropopvvv  7300  oaord  7672  oeeu  7728  nnaord  7744  swoso  7820  fiint  8278  funsnfsupp  8340  alephval3  8971  fpwwe2lem8  9497  fpwwe2lem9  9498  fpwwe2lem12  9501  ingru  9675  axgroth3  9691  ltrelxr  10137  ltxrlt  10146  wloglei  10598  sup2  11017  rexuz2  11777  ltxr  11987  elixx3g  12226  ixxun  12229  elioo4g  12272  elioopnf  12305  elioomnf  12306  elicopnf  12307  elxrge0  12319  divelunit  12352  elfz2  12371  elfzuzb  12374  uzsplit  12450  fznn0  12470  elfzmlbp  12489  preduz  12500  elfzo2  12512  fzolb2  12516  fzouzsplit  12542  ssfzo12bi  12603  fzind2  12626  ccatsymb  13400  swrdsbslen  13494  swrdspsleq  13495  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccatin12  13537  repsdf2  13571  repswsymball  13572  repswsymballbi  13573  repswswrd  13577  s3eq3seq  13730  wrdl3s3  13751  s3sndisj  13752  s3iunsndisj  13753  abs2dif  14116  sinltx  14963  divalglem8  15170  divalglem10  15172  divalgb  15174  bitsval2  15194  divgcdz  15280  rplpwr  15323  cncongr1  15428  pythagtriplem2  15569  pythagtrip  15586  prmgaplem4  15805  setsstruct2  15943  pwsle  16199  imasvscafn  16244  mreexmrid  16350  iscatd2  16389  issect  16460  issect2  16461  oppcsect  16485  isfunc  16571  funcpropd  16607  fucsect  16679  fucinv  16680  initoeu2  16713  setcsect  16786  setcinv  16787  issubm2  17395  issubg3  17659  resgrpisgrp  17662  cycsubgcl  17667  eqgval  17690  eqger  17691  isgim  17751  gaorb  17786  gaorber  17787  gastacos  17789  symg2bas  17864  galactghm  17869  gsmsymgreqlem2  17897  pmtr3ncom  17941  ispgp  18053  efgcpbllema  18213  efgcpbllemb  18214  eqgabl  18286  dprdw  18455  ringpropd  18628  ringrghm  18651  isirred2  18747  rim0to0  18790  drngid2  18811  islss  18983  islmim  19110  lmhmpropd  19121  isassa  19363  mpfrcl  19566  zndvds  19946  znleval  19951  znleval2  19952  obselocv  20120  matinvgcell  20289  mat1dimscm  20329  scmatscm  20367  scmatf1  20385  mdetunilem7  20472  cpmatacl  20569  cpmatmcl  20572  mat2pmatf1  20582  mat2pmatghm  20583  mat2pmatmul  20584  mat2pmatlin  20588  mat2pmatscmxcl  20593  m2pmfzgsumcl  20601  decpmataa0  20621  monmatcollpw  20632  pmatcollpwscmatlem1  20642  pmatcollpwscmatlem2  20643  pm2mpghm  20669  pm2mpmhmlem2  20672  monmat2matmon  20677  chfacfisf  20707  chfacfisfcpmat  20708  chfacfpmmulgsum2  20718  isbasis3g  20801  leordtvallem2  21063  lmfval  21084  lmbr  21110  lmbr2  21111  lmmo  21232  dfconn2  21270  ptbasin  21428  ptbasfi  21432  txcnpi  21459  ptcnp  21473  hausdiag  21496  qtophmeo  21668  fbunfip  21720  elflim2  21815  hausflimi  21831  isfcls  21860  isfcls2  21864  istmd  21925  istgp  21928  istrg  22014  istdrg  22016  istdrg2  22028  istlm  22035  imasdsf1olem  22225  xmeterval  22284  xmeter  22285  prdsxmslem2  22381  blval2  22414  isngp  22447  isngp2  22448  isngp3  22449  isnlm  22526  cnbl0  22624  cnblcld  22625  elii1  22781  isphtpc  22840  phtpcer  22841  isclmp  22943  iscph  23016  lmmbr  23102  lmmbr2  23103  lmmbrf  23106  iscfil2  23110  iscau3  23122  iscau4  23123  iscauf  23124  caucfil  23127  isbn  23181  ishl2  23212  ovolfcl  23281  ioombl1lem4  23375  mbfmax  23461  iblpos  23604  limcrcl  23683  ig1pval3  23979  ulmdvlem3  24201  ellogdm  24430  relogbcl  24556  fsumvma2  24984  chpchtsum  24989  chpub  24990  dchrelbas3  25008  gausslemma2dlem1a  25135  lnhl  25555  colopp  25706  dfcgra2  25766  axeuclidlem  25887  axeuclid  25888  edgupgr  26074  umgr2edg1  26148  subusgr  26226  nbgrel  26278  nb3grpr2  26329  nb3gr2nb  26330  isuvtx  26343  isuvtxaOLD  26344  nbupgruvtxres  26358  iscplgredg  26369  cplgr3v  26387  rusgrpropedg  26536  rgrusgrprc  26541  rusgrprc  26542  upgriswlk  26593  wlkonprop  26610  wksonproplem  26657  usgr2pth0  26717  isclwlke  26729  crctcshtrl  26771  iswwlksnx  26788  wwlknbp  26790  2trld  26903  rusgrnumwwlkl1  26935  rusgrnumwwlkb0  26938  rusgrnumwwlk  26942  erclwwlkref  26977  clwwlkwwlksb  27018  erclwwlknref  27033  clwlksf1clwwlklem0  27051  clwwlknonelOLD  27071  clwwlknon2x  27078  0wlk  27094  3spthd  27154  umgr3v3e3cycl  27162  frgr3v  27255  1to3vfriswmgr  27260  frgr2wwlkeu  27307  numclwlk1lem2fo  27348  nvex  27594  isnv  27595  dfadj2  28872  cnvadj  28879  adjeq  28922  eleigvec  28944  eleigvec2  28945  chirredi  29381  or3di  29435  dfrp2  29660  eliccelico  29667  omndmul2  29840  isorng  29927  pmtrprfv2  29976  fzto1st  29981  psgnfzto1st  29983  eulerpartlemv  30554  eulerpartlemd  30556  eulerpartlemn  30571  prob01  30603  probun  30609  bnj170  30892  bnj248  30894  bnj252  30897  bnj253  30898  bnj945  30970  bnj1098  30980  bnj1224  30998  bnj150  31072  bnj153  31076  bnj545  31091  bnj557  31097  bnj571  31102  bnj594  31108  bnj864  31118  bnj865  31119  bnj849  31121  bnj964  31139  bnj986  31150  bnj996  31151  bnj1033  31163  bnj1110  31176  bnj1128  31184  bnj1174  31197  pconnconn  31339  resconn  31354  iscvm  31367  cvmlift2lem12  31422  cvmlift3lem5  31431  elmpst  31559  mpstrcl  31564  lediv2aALT  31697  dfso3  31727  br6  31773  etasslt  32045  elfuns  32147  brimg  32169  brsuccf  32173  cgrxfr  32287  segcon2  32337  seglecgr12im  32342  seglecgr12  32343  segletr  32346  btwnoutside  32357  broutsideof3  32358  outsideoftr  32361  outsidele  32364  bj-imn3ani  32697  relowlpssretop  33342  lindsenlbs  33534  matunitlindflem2  33536  fdc  33671  isbnd3b  33714  ablo4pnp  33809  crngm4  33932  isidlc  33944  pridl  33966  ispridl2  33967  ispridlc  33999  ts3an1  34087  ts3an2  34088  ts3an3  34089  brres2  34176  eldmqsres  34192  xrninxp  34290  xrninxp2  34291  islshpsm  34585  islshpat  34622  cmtfvalN  34815  cmtvalN  34816  ishlat1  34957  ishlat2  34958  3dim0  35061  2dim  35074  islvol5  35183  lhpexle3  35616  cdleme0ex2N  35829  cdleme0nex  35895  cdlemg2cex  36196  cdlemg33b0  36306  cdlemg33b  36312  cdlemg33c  36313  cdlemg33e  36315  dib1dim  36771  diblsmopel  36777  dihopelvalcpre  36854  lcfls1c  37142  3anrabdioph  37663  issdrg2  38085  fgraphxp  38106  dfrtrcl5  38253  brfvrcld2  38301  df3an2  38378  dfvd3  39124  3impexpVD  39405  rfcnnnub  39509  stoweidlem35  40570  smflimlem4  41303  ndmaovass  41607  nltle2tri  41648  elfz2z  41650  pfxccatin12lem2  41749  pfxccatin12  41750  pfxccat3a  41754  gboge9  41977  sbgoldbalt  41994  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  bgoldbtbndlem4  42021  bgoldbtbnd  42022  ismhm0  42130  rnglz  42209  rngcsect  42305  rngcinv  42306  rngcsectALTV  42317  rngcinvALTV  42318  ringcsect  42356  ringcinv  42357  ringcsectALTV  42380  ringcinvALTV  42381  islindeps  42567  islindeps2  42597  isldepslvec2  42599  elbigo2  42671
  Copyright terms: Public domain W3C validator