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 1038
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 680. (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 1036 . 2 wff (𝜑𝜓𝜒)
51, 2wa 384 . . 3 wff (𝜑𝜓)
65, 3wa 384 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 196 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1040  3anrot  1041  3ancoma  1043  3anan32  1048  3anor  1052  3ioran  1054  3simpa  1056  3pm3.2i  1237  pm3.2an3  1238  pm3.2an3OLD  1239  3jca  1240  3anbi123i  1249  3imp  1254  3an4anass  1288  3anbi123d  1396  3anim123d  1403  an6  1405  an3andi  1442  an33rean  1443  cadan  1545  19.26-3an  1797  nf3and  1824  nf3an  1828  4exdistr  1921  eeeanv  2182  nf3andOLD  2232  nf3anOLD  2238  sb3an  2399  mopick2  2539  r3al  2936  r19.26-3  3061  3reeanv  3102  ceqsex3v  3236  ceqsex4v  3237  ceqsex8v  3239  sbc3an  3481  elin3  3788  rexdifpr  4183  raltpg  4214  tpss  4343  dfopif  4374  disjxun  4621  otth2  4922  otthg  4924  oteqex  4934  poirr  5016  po3nr  5019  wefrc  5078  rabxp  5124  brinxp2  5151  brinxp  5152  f1orn  6114  fpropnf1  6489  dff1o6  6496  oprabid  6642  oprabv  6668  ndmovass  6787  elovmpt2  6844  elovmpt2rab  6845  elovmpt2rab1  6846  elovmpt3rab1  6858  dfwe2  6943  opiota  7189  dfxp3  7190  bropopvvv  7215  oaord  7587  oeeu  7643  nnaord  7659  swoso  7735  fiint  8197  funsnfsupp  8259  alephval3  8893  fpwwe2lem8  9419  fpwwe2lem9  9420  fpwwe2lem12  9423  ingru  9597  axgroth3  9613  ltrelxr  10059  ltxrlt  10068  wloglei  10520  sup2  10939  rexuz2  11699  ltxr  11909  elixx3g  12146  ixxun  12149  elioo4g  12192  elioopnf  12225  elioomnf  12226  elicopnf  12227  elxrge0  12239  divelunit  12272  elfz2  12291  elfzuzb  12294  uzsplit  12369  fznn0  12389  elfzmlbp  12407  preduz  12418  elfzo2  12430  fzolb2  12434  fzouzsplit  12460  ssfzo12bi  12520  fzind2  12542  ccatsymb  13321  swrdsbslen  13402  swrdspsleq  13403  swrdccatin2  13440  swrdccatin12lem2  13442  swrdccatin12lem3  13443  swrdccatin12  13444  repsdf2  13478  repswsymball  13479  repswsymballbi  13480  repswswrd  13484  wrdl3s3  13655  s3sndisj  13656  s3iunsndisj  13657  abs2dif  14022  sinltx  14863  divalglem8  15066  divalglem10  15068  divalgb  15070  bitsval2  15090  divgcdz  15176  rplpwr  15219  cncongr1  15324  pythagtriplem2  15465  pythagtrip  15482  prmgaplem4  15701  setsstruct2  15836  pwsle  16092  imasvscafn  16137  mreexmrid  16243  iscatd2  16282  issect  16353  issect2  16354  oppcsect  16378  isfunc  16464  funcpropd  16500  fucsect  16572  fucinv  16573  initoeu2  16606  setcsect  16679  setcinv  16680  issubm2  17288  issubg3  17552  resgrpisgrp  17555  cycsubgcl  17560  eqgval  17583  eqger  17584  isgim  17644  gaorb  17680  gaorber  17681  gastacos  17683  symg2bas  17758  galactghm  17763  gsmsymgreqlem2  17791  pmtr3ncom  17835  ispgp  17947  efgcpbllema  18107  efgcpbllemb  18108  eqgabl  18180  dprdw  18349  ringpropd  18522  ringrghm  18545  isirred2  18641  rim0to0  18682  drngid2  18703  islss  18875  islmim  19002  lmhmpropd  19013  isassa  19255  mpfrcl  19458  zndvds  19838  znleval  19843  znleval2  19844  obselocv  20012  matinvgcell  20181  mat1dimscm  20221  scmatscm  20259  scmatf1  20277  mdetunilem7  20364  cpmatacl  20461  cpmatmcl  20464  mat2pmatf1  20474  mat2pmatghm  20475  mat2pmatmul  20476  mat2pmatlin  20480  mat2pmatscmxcl  20485  m2pmfzgsumcl  20493  decpmataa0  20513  monmatcollpw  20524  pmatcollpwscmatlem1  20534  pmatcollpwscmatlem2  20535  pm2mpghm  20561  pm2mpmhmlem2  20564  monmat2matmon  20569  chfacfisf  20599  chfacfisfcpmat  20600  chfacfpmmulgsum2  20610  isbasis3g  20693  leordtvallem2  20955  lmfval  20976  lmbr  21002  lmbr2  21003  lmmo  21124  dfconn2  21162  ptbasin  21320  ptbasfi  21324  txcnpi  21351  ptcnp  21365  hausdiag  21388  qtophmeo  21560  fbunfip  21613  elflim2  21708  hausflimi  21724  isfcls  21753  isfcls2  21757  istmd  21818  istgp  21821  istrg  21907  istdrg  21909  istdrg2  21921  istlm  21928  imasdsf1olem  22118  xmeterval  22177  xmeter  22178  prdsxmslem2  22274  blval2  22307  isngp  22340  isngp2  22341  isngp3  22342  isnlm  22419  cnbl0  22517  cnblcld  22518  elii1  22674  isphtpc  22733  phtpcer  22734  phtpcerOLD  22735  isclmp  22837  iscph  22910  lmmbr  22996  lmmbr2  22997  lmmbrf  23000  iscfil2  23004  iscau3  23016  iscau4  23017  iscauf  23018  caucfil  23021  isbn  23075  ishl2  23106  ovolfcl  23175  ioombl1lem4  23269  mbfmax  23356  iblpos  23499  limcrcl  23578  ig1pval3  23872  ulmdvlem3  24094  ellogdm  24319  relogbcl  24445  fsumvma2  24873  chpchtsum  24878  chpub  24879  dchrelbas3  24897  gausslemma2dlem1a  25024  lnhl  25444  colopp  25595  dfcgra2  25655  axeuclidlem  25776  axeuclid  25777  edgupgr  25958  umgr2edg1  26030  subusgr  26108  nb3grpr2  26206  nb3gr2nb  26207  isuvtxa  26216  nbupgruvtxres  26229  iscplgredg  26234  cplgr3v  26252  rusgrpropedg  26384  rgrusgrprc  26389  rusgrprc  26390  upgriswlk  26440  wlkonprop  26457  wksonproplem  26504  usgr2pth0  26564  isclwlke  26576  crctcshtrl  26618  iswwlksnx  26634  wwlknbp  26636  2trld  26737  rusgrnumwwlkl1  26764  rusgrnumwwlkb0  26767  rusgrnumwwlk  26771  erclwwlksref  26834  erclwwlksnref  26846  clwlksf1clwwlklem0  26864  0wlk  26877  3spthd  26936  umgr3v3e3cycl  26944  frgr3v  27037  1to3vfriswmgr  27042  frgr2wwlkeu  27084  extwwlkfablem2  27102  numclwwlkovfel2  27106  numclwwlkovf2  27107  numclwlk1lem2fo  27117  nvex  27354  isnv  27355  dfadj2  28632  cnvadj  28639  adjeq  28682  eleigvec  28704  eleigvec2  28705  chirredi  29141  or3di  29195  dfrp2  29417  eliccelico  29424  omndmul2  29539  isorng  29626  pmtrprfv2  29675  fzto1st  29680  psgnfzto1st  29682  eulerpartlemv  30249  eulerpartlemd  30251  eulerpartlemn  30266  prob01  30298  probun  30304  bnj170  30524  bnj248  30526  bnj252  30529  bnj253  30530  bnj945  30605  bnj1098  30615  bnj1224  30633  bnj150  30707  bnj153  30711  bnj545  30726  bnj557  30732  bnj571  30737  bnj594  30743  bnj864  30753  bnj865  30754  bnj849  30756  bnj964  30774  bnj986  30785  bnj996  30786  bnj1033  30798  bnj1110  30811  bnj1128  30819  bnj1174  30832  pconnconn  30974  resconn  30989  iscvm  31002  cvmlift2lem12  31057  cvmlift3lem5  31066  elmpst  31194  mpstrcl  31199  lediv2aALT  31332  dfso3  31363  br6  31408  elfuns  31717  brimg  31739  brsuccf  31743  cgrxfr  31857  segcon2  31907  seglecgr12im  31912  seglecgr12  31913  segletr  31916  btwnoutside  31927  broutsideof3  31928  outsideoftr  31931  outsidele  31934  bj-imn3ani  32267  relowlpssretop  32883  lindsenlbs  33075  matunitlindflem2  33077  fdc  33212  isbnd3b  33255  ablo4pnp  33350  crngm4  33473  isidlc  33485  pridl  33507  ispridl2  33508  ispridlc  33540  ts3an1  33628  ts3an2  33629  ts3an3  33630  islshpsm  33786  islshpat  33823  cmtfvalN  34016  cmtvalN  34017  ishlat1  34158  ishlat2  34159  3dim0  34262  2dim  34275  islvol5  34384  lhpexle3  34817  cdleme0ex2N  35030  cdleme0nex  35096  cdlemg2cex  35398  cdlemg33b0  35508  cdlemg33b  35514  cdlemg33c  35515  cdlemg33e  35517  dib1dim  35973  diblsmopel  35979  dihopelvalcpre  36056  lcfls1c  36344  3anrabdioph  36865  issdrg2  37288  fgraphxp  37309  dfrtrcl5  37456  brfvrcld2  37504  df3an2  37581  dfvd3  38328  3impexpVD  38613  rfcnnnub  38717  stoweidlem35  39589  smflimlem4  40319  ndmaovass  40620  nltle2tri  40650  elfz2z  40652  pfxccatin12lem2  40753  pfxccatin12  40754  pfxccat3a  40758  gboage9  40977  sgoldbalt  40994  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  bgoldbtbndlem4  41015  bgoldbtbnd  41016  ismhm0  41123  rnglz  41202  rngcsect  41298  rngcinv  41299  rngcsectALTV  41310  rngcinvALTV  41311  ringcsect  41349  ringcinv  41350  ringcsectALTV  41373  ringcinvALTV  41374  islindeps  41560  islindeps2  41590  isldepslvec2  41592  elbigo2  41668
  Copyright terms: Public domain W3C validator