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 1081
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 469. (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 1079 . 2 wff (𝜑𝜓𝜒)
51, 2wa 396 . . 3 wff (𝜑𝜓)
65, 3wa 396 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 207 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1087  3anan32  1089  3ancomb  1091  3anidm  1096  3an4anass  1097  3ioran  1098  3ianor  1099  3impa  1102  3expa  1110  3jca  1120  3anbi123i  1147  3pm3.2i  1331  3anbi123d  1427  3anim123d  1434  an6  1436  an3andi  1473  an33rean  1474  cadan  1601  19.26-3an  1864  nf3and  1890  nf3an  1893  4exdistr  1954  sb3an  2078  eeeanv  2363  mopick2  2718  r19.26-3  3172  r3al  3202  3reeanv  3369  ceqsex3v  3546  ceqsex4v  3547  ceqsex8v  3549  sbc3an  3837  elin3  4176  rexdifpr  4590  raltpg  4628  tpss  4762  opthprneg  4789  dfopif  4794  disjxun  5056  otth2  5367  otthg  5369  oteqex  5382  poirr  5479  po3nr  5482  wefrc  5543  rabxp  5594  f1orn  6619  fpropnf1  7016  dff1o6  7023  oprabidw  7176  oprabid  7177  oprabv  7203  ndmovass  7325  elovmpo  7379  elovmporab  7380  elovmporab1w  7381  elovmporab1  7382  elovmpt3rab1  7394  dfwe2  7484  opiota  7748  dfxp3  7750  bropopvvv  7776  oaord  8163  oeeu  8219  nnaord  8235  swoso  8312  fiint  8784  funsnfsupp  8846  alephval3  9525  ingru  10226  axgroth3  10242  ltrelxr  10691  ltxrlt  10700  wloglei  11161  sup2  11586  rexuz2  12288  ltxr  12500  elixx3g  12741  ixxun  12744  elioo4g  12787  elioopnf  12821  elioomnf  12822  elicopnf  12823  elxrge0  12835  divelunit  12870  elfz2  12889  elfzuzb  12892  uzsplit  12969  fznn0  12989  elfzmlbp  13008  preduz  13019  elfzo2  13031  fzolb2  13035  fzouzsplit  13062  ssfzo12bi  13122  fzind2  13145  hashgt23el  13775  ccatsymb  13926  swrdsbslen  14016  swrdspsleq  14017  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  pfxccatin12  14085  pfxccat3a  14090  repsdf2  14130  repswsymball  14131  repswsymballbi  14132  repswswrd  14136  s3eq3seq  14291  wrdl3s3  14316  s3sndisj  14317  s3iunsndisj  14318  abs2dif  14682  sinltx  15532  divalglem8  15741  divalglem10  15743  divalgb  15745  bitsval2  15764  divgcdz  15850  rplpwr  15897  cncongr1  16001  pythagtriplem2  16144  pythagtrip  16161  prmgaplem4  16380  isstruct  16486  setsstruct2  16511  imasvscafn  16800  xpscf  16828  mreexmrid  16904  iscatd2  16942  issect  17013  issect2  17014  oppcsect  17038  isfunc  17124  funcpropd  17160  fucsect  17232  fucinv  17233  initoeu2  17266  setcsect  17339  setcinv  17340  issubm2  17959  issubg3  18237  resgrpisgrp  18240  eqgval  18269  eqger  18270  cycsubgcl  18289  isgim  18342  gaorb  18377  gaorber  18378  gastacos  18380  symg2bas  18457  galactghm  18463  pmtr3ncom  18534  ispgp  18648  efgcpbllema  18811  efgcpbllemb  18812  eqgabl  18886  cygabl  18941  dprdw  19063  ringpropd  19263  ringrghm  19286  isirred2  19382  gim0to0  19426  rim0to0OLD  19427  drngid2  19449  issdrg2  19508  islss  19637  islmim  19765  lmhmpropd  19776  isassa  20018  mpfrcl  20228  zndvds  20626  znleval  20631  znleval2  20632  obselocv  20802  matinvgcell  20974  mat1dimscm  21014  scmatscm  21052  scmatf1  21070  mdetunilem7  21157  cpmatacl  21254  cpmatmcl  21257  mat2pmatf1  21267  mat2pmatghm  21268  mat2pmatmul  21269  mat2pmatlin  21273  mat2pmatscmxcl  21278  m2pmfzgsumcl  21286  decpmataa0  21306  monmatcollpw  21317  pmatcollpwscmatlem1  21327  pmatcollpwscmatlem2  21328  pm2mpghm  21354  pm2mpmhmlem2  21357  monmat2matmon  21362  chfacfisf  21392  chfacfisfcpmat  21393  chfacfpmmulgsum2  21403  isbasis3g  21487  leordtvallem2  21749  lmfval  21770  lmbr  21796  lmbr2  21797  lmmo  21918  dfconn2  21957  ptbasin  22115  ptbasfi  22119  txcnpi  22146  ptcnp  22160  hausdiag  22183  qtophmeo  22355  fbunfip  22407  elflim2  22502  hausflimi  22518  isfcls  22547  isfcls2  22551  istmd  22612  istgp  22615  istrg  22701  istdrg  22703  istdrg2  22715  istlm  22722  imasdsf1olem  22912  xmeterval  22971  xmeter  22972  prdsxmslem2  23068  blval2  23101  isngp  23134  isngp2  23135  isngp3  23136  isnlm  23213  cnbl0  23311  cnblcld  23312  elii1  23468  isphtpc  23527  phtpcer  23528  isclmp  23630  iscph  23703  lmmbr  23790  lmmbr2  23791  lmmbrf  23794  iscfil2  23798  iscau3  23810  iscau4  23811  iscauf  23812  caucfil  23815  isbn  23870  ishl2  23902  ovolfcl  23996  ioombl1lem4  24091  mbfmax  24179  iblpos  24322  limcrcl  24401  ig1pval3  24697  ulmdvlem3  24919  ellogdm  25149  relogbcl  25278  fsumvma2  25718  chpchtsum  25723  chpub  25724  dchrelbas3  25742  gausslemma2dlem1a  25869  lnhl  26329  colopp  26483  dfcgra2  26544  axeuclidlem  26676  axeuclid  26677  edgupgr  26847  umgr2edg1  26921  subusgr  26999  nbgrel  27050  nb3grpr2  27093  nb3gr2nb  27094  isuvtx  27105  nbupgruvtxres  27117  iscplgredg  27127  cplgr3v  27145  rusgrpropedg  27294  rgrusgrprc  27299  rusgrprc  27300  upgriswlk  27350  wlkonprop  27368  wksonproplem  27414  usgr2pth0  27474  isclwlke  27486  crctcshtrl  27529  iswwlksnx  27546  wwlknbp  27548  2trld  27645  rusgrnumwwlkl1  27675  rusgrnumwwlkb0  27678  rusgrnumwwlk  27682  clwlkclwwlkflem  27710  erclwwlkref  27726  clwwlkwwlksb  27761  erclwwlknref  27776  clwwlknon2x  27810  0wlk  27823  3spthd  27883  umgr3v3e3cycl  27891  frgr3v  27982  1to3vfriswmgr  27987  frgr2wwlkeu  28034  numclwwlk1lem2fo  28065  dlwwlknondlwlknonf1o  28072  nvex  28316  isnv  28317  dfadj2  29590  cnvadj  29597  adjeq  29640  eleigvec  29662  eleigvec2  29663  chirredi  30099  or3di  30153  dfrp2  30418  eliccelico  30427  omndmul2  30641  pmtrprfv2  30660  fzto1st  30673  psgnfzto1st  30675  isorng  30800  qusker  30846  qusxpid  30856  eulerpartlemv  31522  eulerpartlemd  31524  eulerpartlemn  31539  prob01  31571  probun  31577  bnj170  31868  bnj248  31870  bnj252  31873  bnj253  31874  bnj945  31945  bnj1098  31955  bnj1224  31973  bnj150  32048  bnj153  32052  bnj545  32067  bnj557  32073  bnj571  32078  bnj594  32084  bnj864  32094  bnj865  32095  bnj849  32097  bnj964  32115  bnj986  32126  bnj996  32127  bnj1033  32139  bnj1110  32152  bnj1128  32160  bnj1174  32173  subgrwlk  32277  cusgr3cyclex  32281  loop1cycl  32282  2cycl2d  32284  pconnconn  32376  resconn  32391  iscvm  32404  cvmlift2lem12  32459  cvmlift3lem5  32468  satfdm  32514  elmpst  32681  mpstrcl  32686  lediv2aALT  32818  dfso3  32848  br6  32891  etasslt  33172  elfuns  33274  brimg  33296  brsuccf  33300  cgrxfr  33414  segcon2  33464  seglecgr12im  33469  seglecgr12  33470  segletr  33473  btwnoutside  33484  broutsideof3  33485  outsideoftr  33488  outsidele  33491  bj-imn3ani  33819  relowlpssretop  34528  lindsenlbs  34769  matunitlindflem2  34771  fdc  34903  isbnd3b  34946  ablo4pnp  35041  crngm4  35164  isidlc  35176  pridl  35198  ispridl2  35199  ispridlc  35231  ts3an1  35311  ts3an2  35312  ts3an3  35313  brres2  35412  xrninxp  35522  dfeqvrels2  35705  dfeqvrel2  35707  dfeqvrel3  35708  dfeldisj3  35834  islshpsm  35998  islshpat  36035  cmtfvalN  36228  cmtvalN  36229  ishlat1  36370  ishlat2  36371  3dim0  36475  2dim  36488  islvol5  36597  lhpexle3  37030  cdleme0ex2N  37242  cdleme0nex  37308  cdlemg2cex  37609  cdlemg33b0  37719  cdlemg33b  37725  cdlemg33c  37726  cdlemg33e  37728  dib1dim  38183  diblsmopel  38189  dihopelvalcpre  38266  lcfls1c  38554  3anrabdioph  39259  fgraphxp  39691  dfsucon  39769  pren2  39792  dfrtrcl5  39869  brfvrcld2  39917  df3an2  39994  dfvd3  40805  3impexpVD  41070  rfcnnnub  41173  stoweidlem35  42201  smflimlem4  42931  ndmaovass  43286  nltle2tri  43394  elfz2z  43396  prproropf1olem0  43511  reuprpr  43532  gboge9  43776  sbgoldbalt  43793  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  bgoldbtbndlem4  43820  bgoldbtbnd  43821  ismhm0  43919  rnglz  44053  rngcsect  44149  rngcinv  44150  rngcsectALTV  44161  rngcinvALTV  44162  ringcsect  44200  ringcinv  44201  ringcsectALTV  44224  ringcinvALTV  44225  islindeps  44406  islindeps2  44436  isldepslvec2  44438  elbigo2  44510  line2ylem  44636
  Copyright terms: Public domain W3C validator