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 1086
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 472. (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 1084 . 2 wff (𝜑𝜓𝜒)
51, 2wa 399 . . 3 wff (𝜑𝜓)
65, 3wa 399 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 209 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1092  3anan32  1094  3ancomb  1096  3anidm  1101  3an4anass  1102  3ioran  1103  3ianor  1104  3impa  1107  3expa  1115  3jca  1125  3anbi123i  1152  3pm3.2i  1336  3anbi123d  1433  3anim123d  1440  an6  1442  an3andi  1479  an33rean  1480  an33reanOLD  1481  cadan  1611  19.26-3an  1873  nf3and  1899  nf3an  1902  4exdistr  1963  sb3an  2086  eeeanv  2363  mopick2  2702  r19.26-3  3142  r3al  3170  3reeanv  3324  ceqsex3v  3496  ceqsex4v  3497  ceqsex8v  3499  sbc3an  3788  elin3  4130  rexdifpr  4561  raltpg  4597  tpss  4731  opthprneg  4758  dfopif  4763  disjxun  5031  otth2  5343  otthg  5345  oteqex  5358  poirr  5453  po3nr  5456  wefrc  5517  rabxp  5568  f1orn  6604  fpropnf1  7007  dff1o6  7014  oprabidw  7170  oprabid  7171  oprabv  7197  ndmovass  7320  elovmpo  7374  elovmporab  7375  elovmporab1w  7376  elovmporab1  7377  elovmpt3rab1  7389  dfwe2  7480  opiota  7743  dfxp3  7745  bropopvvv  7772  oaord  8160  oeeu  8216  nnaord  8232  swoso  8309  fiint  8783  funsnfsupp  8845  alephval3  9525  ingru  10230  axgroth3  10246  ltrelxr  10695  ltxrlt  10704  wloglei  11165  sup2  11588  rexuz2  12291  ltxr  12502  elixx3g  12743  ixxun  12746  elioo4g  12789  elioopnf  12825  elioomnf  12826  elicopnf  12827  elxrge0  12839  divelunit  12876  elfz2  12896  elfzuzb  12900  uzsplit  12978  fznn0  12998  elfzmlbp  13017  preduz  13028  elfzo2  13040  fzolb2  13044  fzouzsplit  13071  ssfzo12bi  13131  fzind2  13154  hashgt23el  13785  ccatsymb  13931  swrdsbslen  14021  swrdspsleq  14022  swrdccatin2  14086  pfxccatin12lem2  14088  pfxccatin12lem3  14089  pfxccatin12  14090  pfxccat3a  14095  repsdf2  14135  repswsymball  14136  repswsymballbi  14137  repswswrd  14141  s3eq3seq  14296  wrdl3s3  14321  s3sndisj  14322  s3iunsndisj  14323  abs2dif  14687  sinltx  15537  divalglem8  15744  divalglem10  15746  divalgb  15748  bitsval2  15767  divgcdz  15853  rplpwr  15900  cncongr1  16004  pythagtriplem2  16147  pythagtrip  16164  prmgaplem4  16383  isstruct  16491  setsstruct2  16516  imasvscafn  16805  xpscf  16833  mreexmrid  16909  iscatd2  16947  issect  17018  issect2  17019  oppcsect  17043  isfunc  17129  funcpropd  17165  fucsect  17237  fucinv  17238  initoeu2  17271  setcsect  17344  setcinv  17345  issubm2  17964  issubg3  18292  resgrpisgrp  18295  eqgval  18324  eqger  18325  cycsubgcl  18344  isgim  18397  gaorb  18432  gaorber  18433  gastacos  18435  symg2bas  18516  galactghm  18527  pmtr3ncom  18598  ispgp  18712  efgcpbllema  18875  efgcpbllemb  18876  eqgabl  18951  cygabl  19006  dprdw  19128  ringpropd  19331  ringrghm  19354  isirred2  19450  gim0to0  19493  drngid2  19514  issdrg2  19573  islss  19702  islmim  19830  lmhmpropd  19841  zndvds  20244  znleval  20249  znleval2  20250  obselocv  20420  isassa  20548  mpfrcl  20760  matinvgcell  21043  mat1dimscm  21083  scmatscm  21121  scmatf1  21139  mdetunilem7  21226  cpmatacl  21324  cpmatmcl  21327  mat2pmatf1  21337  mat2pmatghm  21338  mat2pmatmul  21339  mat2pmatlin  21343  mat2pmatscmxcl  21348  m2pmfzgsumcl  21356  decpmataa0  21376  monmatcollpw  21387  pmatcollpwscmatlem1  21397  pmatcollpwscmatlem2  21398  pm2mpghm  21424  pm2mpmhmlem2  21427  monmat2matmon  21432  chfacfisf  21462  chfacfisfcpmat  21463  chfacfpmmulgsum2  21473  isbasis3g  21557  leordtvallem2  21819  lmfval  21840  lmbr  21866  lmbr2  21867  lmmo  21988  dfconn2  22027  ptbasin  22185  ptbasfi  22189  txcnpi  22216  ptcnp  22230  hausdiag  22253  qtophmeo  22425  fbunfip  22477  elflim2  22572  hausflimi  22588  isfcls  22617  isfcls2  22621  istmd  22682  istgp  22685  istrg  22772  istdrg  22774  istdrg2  22786  istlm  22793  imasdsf1olem  22983  xmeterval  23042  xmeter  23043  prdsxmslem2  23139  blval2  23172  isngp  23205  isngp2  23206  isngp3  23207  isnlm  23284  cnbl0  23382  cnblcld  23383  elii1  23543  isphtpc  23602  phtpcer  23603  isclmp  23705  iscph  23778  lmmbr  23865  lmmbr2  23866  lmmbrf  23869  iscfil2  23873  iscau3  23885  iscau4  23886  iscauf  23887  caucfil  23890  isbn  23945  ishl2  23977  ovolfcl  24073  ioombl1lem4  24168  mbfmax  24256  iblpos  24399  limcrcl  24480  ig1pval3  24778  ulmdvlem3  25000  ellogdm  25233  relogbcl  25362  fsumvma2  25801  chpchtsum  25806  chpub  25807  dchrelbas3  25825  gausslemma2dlem1a  25952  lnhl  26412  colopp  26566  dfcgra2  26627  axeuclidlem  26759  axeuclid  26760  edgupgr  26930  umgr2edg1  27004  subusgr  27082  nbgrel  27133  nb3grpr2  27176  nb3gr2nb  27177  isuvtx  27188  nbupgruvtxres  27200  iscplgredg  27210  cplgr3v  27228  rusgrpropedg  27377  rgrusgrprc  27382  rusgrprc  27383  upgriswlk  27433  wlkonprop  27451  wksonproplem  27497  usgr2pth0  27557  isclwlke  27569  crctcshtrl  27612  iswwlksnx  27629  wwlknbp  27631  2trld  27727  rusgrnumwwlkl1  27757  rusgrnumwwlkb0  27760  rusgrnumwwlk  27764  clwlkclwwlkflem  27792  erclwwlkref  27808  clwwlkwwlksb  27842  erclwwlknref  27857  clwwlknon2x  27891  0wlk  27904  3spthd  27964  umgr3v3e3cycl  27972  frgr3v  28063  1to3vfriswmgr  28068  frgr2wwlkeu  28115  numclwwlk1lem2fo  28146  dlwwlknondlwlknonf1o  28153  nvex  28397  isnv  28398  dfadj2  29671  cnvadj  29678  adjeq  29721  eleigvec  29743  eleigvec2  29744  chirredi  30180  or3di  30234  dfrp2  30520  eliccelico  30529  omndmul2  30766  pmtrprfv2  30785  fzto1st  30798  psgnfzto1st  30800  isorng  30926  qusker  30972  qusxpid  30982  lsmsnorb  31002  prmidl0  31034  eulerpartlemv  31730  eulerpartlemd  31732  eulerpartlemn  31747  prob01  31779  probun  31785  bnj170  32076  bnj248  32078  bnj252  32081  bnj253  32082  bnj945  32153  bnj1098  32163  bnj1224  32181  bnj150  32256  bnj153  32260  bnj545  32275  bnj557  32281  bnj571  32286  bnj594  32292  bnj864  32302  bnj865  32303  bnj849  32305  bnj964  32323  bnj986  32335  bnj996  32336  bnj1033  32349  bnj1110  32362  bnj1128  32370  bnj1174  32383  subgrwlk  32487  cusgr3cyclex  32491  loop1cycl  32492  2cycl2d  32494  pconnconn  32586  resconn  32601  iscvm  32614  cvmlift2lem12  32669  cvmlift3lem5  32678  satfdm  32724  elmpst  32891  mpstrcl  32896  lediv2aALT  33028  dfso3  33058  br6  33101  etasslt  33382  elfuns  33484  brimg  33506  brsuccf  33510  cgrxfr  33624  segcon2  33674  seglecgr12im  33679  seglecgr12  33680  segletr  33683  btwnoutside  33694  broutsideof3  33695  outsideoftr  33698  outsidele  33701  bj-imn3ani  34029  relowlpssretop  34776  wl-df3-3mintru2  34896  lindsenlbs  35045  matunitlindflem2  35047  fdc  35176  isbnd3b  35216  ablo4pnp  35311  crngm4  35434  isidlc  35446  pridl  35468  ispridl2  35469  ispridlc  35501  ts3an1  35581  ts3an2  35582  ts3an3  35583  brres2  35682  xrninxp  35793  dfeqvrels2  35976  dfeqvrel2  35978  dfeqvrel3  35979  dfeldisj3  36105  islshpsm  36269  islshpat  36306  cmtfvalN  36499  cmtvalN  36500  ishlat1  36641  ishlat2  36642  3dim0  36746  2dim  36759  islvol5  36868  lhpexle3  37301  cdleme0ex2N  37513  cdleme0nex  37579  cdlemg2cex  37880  cdlemg33b0  37990  cdlemg33b  37996  cdlemg33c  37997  cdlemg33e  37999  dib1dim  38454  diblsmopel  38460  dihopelvalcpre  38537  lcfls1c  38825  sn-sup2  39581  3anrabdioph  39710  fgraphxp  40142  dfsucon  40218  pren2  40239  dfrtrcl5  40316  brfvrcld2  40380  df3an2  40457  dfvd3  41284  3impexpVD  41549  rfcnnnub  41652  stoweidlem35  42664  smflimlem4  43394  ndmaovass  43749  nltle2tri  43857  elfz2z  43859  prproropf1olem0  44006  reuprpr  44027  gboge9  44269  sbgoldbalt  44286  nnsum4primesodd  44301  nnsum4primesoddALTV  44302  bgoldbtbndlem4  44313  bgoldbtbnd  44314  ismhm0  44412  rnglz  44495  rngcsect  44591  rngcinv  44592  rngcsectALTV  44603  rngcinvALTV  44604  ringcsect  44642  ringcinv  44643  ringcsectALTV  44666  ringcinvALTV  44667  islindeps  44849  islindeps2  44879  isldepslvec2  44881  elbigo2  44953  line2ylem  45152
  Copyright terms: Public domain W3C validator