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 1074
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 684. (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 1072 . 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  1081  3anan32  1083  3ancomaOLD  1085  3ancomb  1086  3anrotOLD  1089  3anorOLD  1094  3ioran  1095  3ianor  1096  3impa  1100  3impOLD  1102  3expa  1111  3jca  1122  3simpaOLD  1143  3anbi123i  1158  3pm3.2i  1421  pm3.2an3OLD  1423  3an4anass  1450  3anbi123d  1540  3anim123d  1547  an6  1549  an3andi  1586  an33rean  1587  cadan  1689  19.26-3an  1941  nf3and  1968  nf3an  1972  4exdistr  2028  eeeanv  2320  nf3andOLD  2370  nf3anOLD  2376  sb3an  2529  mopick2  2670  r3al  3070  r19.26-3  3196  3reeanv  3238  ceqsex3v  3378  ceqsex4v  3379  ceqsex8v  3381  sbc3an  3627  elin3  3939  rexdifpr  4342  raltpg  4372  tpss  4505  opthprneg  4537  dfopif  4542  disjxun  4794  otth2  5092  otthg  5094  oteqex  5104  poirr  5190  po3nr  5193  wefrc  5252  rabxp  5303  brinxp2  5329  brinxp  5330  f1orn  6300  fpropnf1  6679  dff1o6  6686  oprabid  6832  oprabv  6860  ndmovass  6979  elovmpt2  7036  elovmpt2rab  7037  elovmpt2rab1  7038  elovmpt3rab1  7050  dfwe2  7138  opiota  7388  dfxp3  7390  bropopvvv  7415  oaord  7788  oeeu  7844  nnaord  7860  swoso  7936  fiint  8394  funsnfsupp  8456  alephval3  9115  fpwwe2lem8  9643  fpwwe2lem9  9644  fpwwe2lem12  9647  ingru  9821  axgroth3  9837  ltrelxr  10283  ltxrlt  10292  wloglei  10744  sup2  11163  rexuz2  11924  ltxr  12134  elixx3g  12373  ixxun  12376  elioo4g  12419  elioopnf  12452  elioomnf  12453  elicopnf  12454  elxrge0  12466  divelunit  12499  elfz2  12518  elfzuzb  12521  uzsplit  12597  fznn0  12617  elfzmlbp  12636  preduz  12647  elfzo2  12659  fzolb2  12663  fzouzsplit  12689  ssfzo12bi  12749  fzind2  12772  ccatsymb  13546  swrdsbslen  13640  swrdspsleq  13641  swrdccatin2  13679  swrdccatin12lem2  13681  swrdccatin12lem3  13682  swrdccatin12  13683  repsdf2  13717  repswsymball  13718  repswsymballbi  13719  repswswrd  13723  s3eq3seq  13876  wrdl3s3  13898  s3sndisj  13899  s3iunsndisj  13900  abs2dif  14263  sinltx  15110  divalglem8  15317  divalglem10  15319  divalgb  15321  bitsval2  15341  divgcdz  15427  rplpwr  15470  cncongr1  15575  pythagtriplem2  15716  pythagtrip  15733  prmgaplem4  15952  setsstruct2  16090  pwsle  16346  imasvscafn  16391  mreexmrid  16497  iscatd2  16535  issect  16606  issect2  16607  oppcsect  16631  isfunc  16717  funcpropd  16753  fucsect  16825  fucinv  16826  initoeu2  16859  setcsect  16932  setcinv  16933  issubm2  17541  issubg3  17805  resgrpisgrp  17808  cycsubgcl  17813  eqgval  17836  eqger  17837  isgim  17897  gaorb  17932  gaorber  17933  gastacos  17935  symg2bas  18010  galactghm  18015  gsmsymgreqlem2  18043  pmtr3ncom  18087  ispgp  18199  efgcpbllema  18359  efgcpbllemb  18360  eqgabl  18432  dprdw  18601  ringpropd  18774  ringrghm  18797  isirred2  18893  rim0to0  18936  drngid2  18957  islss  19129  islmim  19256  lmhmpropd  19267  isassa  19509  mpfrcl  19712  zndvds  20092  znleval  20097  znleval2  20098  obselocv  20266  matinvgcell  20435  mat1dimscm  20475  scmatscm  20513  scmatf1  20531  mdetunilem7  20618  cpmatacl  20715  cpmatmcl  20718  mat2pmatf1  20728  mat2pmatghm  20729  mat2pmatmul  20730  mat2pmatlin  20734  mat2pmatscmxcl  20739  m2pmfzgsumcl  20747  decpmataa0  20767  monmatcollpw  20778  pmatcollpwscmatlem1  20788  pmatcollpwscmatlem2  20789  pm2mpghm  20815  pm2mpmhmlem2  20818  monmat2matmon  20823  chfacfisf  20853  chfacfisfcpmat  20854  chfacfpmmulgsum2  20864  isbasis3g  20947  leordtvallem2  21209  lmfval  21230  lmbr  21256  lmbr2  21257  lmmo  21378  dfconn2  21416  ptbasin  21574  ptbasfi  21578  txcnpi  21605  ptcnp  21619  hausdiag  21642  qtophmeo  21814  fbunfip  21866  elflim2  21961  hausflimi  21977  isfcls  22006  isfcls2  22010  istmd  22071  istgp  22074  istrg  22160  istdrg  22162  istdrg2  22174  istlm  22181  imasdsf1olem  22371  xmeterval  22430  xmeter  22431  prdsxmslem2  22527  blval2  22560  isngp  22593  isngp2  22594  isngp3  22595  isnlm  22672  cnbl0  22770  cnblcld  22771  elii1  22927  isphtpc  22986  phtpcer  22987  isclmp  23089  iscph  23162  lmmbr  23248  lmmbr2  23249  lmmbrf  23252  iscfil2  23256  iscau3  23268  iscau4  23269  iscauf  23270  caucfil  23273  isbn  23327  ishl2  23358  ovolfcl  23427  ioombl1lem4  23521  mbfmax  23607  iblpos  23750  limcrcl  23829  ig1pval3  24125  ulmdvlem3  24347  ellogdm  24576  relogbcl  24702  fsumvma2  25130  chpchtsum  25135  chpub  25136  dchrelbas3  25154  gausslemma2dlem1a  25281  lnhl  25701  colopp  25852  dfcgra2  25912  axeuclidlem  26033  axeuclid  26034  edgupgr  26220  umgr2edg1  26294  subusgr  26372  nbgrel  26424  nb3grpr2  26475  nb3gr2nb  26476  isuvtx  26489  isuvtxaOLD  26490  nbupgruvtxres  26504  iscplgredg  26515  cplgr3v  26533  rusgrpropedg  26682  rgrusgrprc  26687  rusgrprc  26688  upgriswlk  26739  wlkonprop  26756  wksonproplem  26803  usgr2pth0  26863  isclwlke  26875  crctcshtrl  26918  iswwlksnx  26935  wwlknbp  26937  2trld  27050  rusgrnumwwlkl1  27082  rusgrnumwwlkb0  27085  rusgrnumwwlk  27089  clwlkclwwlkflem  27119  erclwwlkref  27135  clwwlkwwlksb  27176  erclwwlknref  27192  clwlksf1clwwlklem0OLD  27210  clwwlknonelOLD  27235  clwwlknon2x  27243  0wlk  27260  3spthd  27320  umgr3v3e3cycl  27328  frgr3v  27421  1to3vfriswmgr  27426  frgr2wwlkeu  27473  numclwlk1lem2fo  27509  dlwwlknondlwlknonf1o  27518  nvex  27767  isnv  27768  dfadj2  29045  cnvadj  29052  adjeq  29095  eleigvec  29117  eleigvec2  29118  chirredi  29554  or3di  29608  dfrp2  29833  eliccelico  29840  omndmul2  30013  isorng  30100  pmtrprfv2  30149  fzto1st  30154  psgnfzto1st  30156  eulerpartlemv  30727  eulerpartlemd  30729  eulerpartlemn  30744  prob01  30776  probun  30782  bnj170  31065  bnj248  31067  bnj252  31070  bnj253  31071  bnj945  31143  bnj1098  31153  bnj1224  31171  bnj150  31245  bnj153  31249  bnj545  31264  bnj557  31270  bnj571  31275  bnj594  31281  bnj864  31291  bnj865  31292  bnj849  31294  bnj964  31312  bnj986  31323  bnj996  31324  bnj1033  31336  bnj1110  31349  bnj1128  31357  bnj1174  31370  pconnconn  31512  resconn  31527  iscvm  31540  cvmlift2lem12  31595  cvmlift3lem5  31604  elmpst  31732  mpstrcl  31737  lediv2aALT  31870  dfso3  31900  br6  31946  etasslt  32218  elfuns  32320  brimg  32342  brsuccf  32346  cgrxfr  32460  segcon2  32510  seglecgr12im  32515  seglecgr12  32516  segletr  32519  btwnoutside  32530  broutsideof3  32531  outsideoftr  32534  outsidele  32537  bj-imn3ani  32870  relowlpssretop  33515  lindsenlbs  33709  matunitlindflem2  33711  fdc  33846  isbnd3b  33889  ablo4pnp  33984  crngm4  34107  isidlc  34119  pridl  34141  ispridl2  34142  ispridlc  34174  ts3an1  34262  ts3an2  34263  ts3an3  34264  brres2  34351  eldmqsres  34367  xrninxp  34465  xrninxp2  34466  islshpsm  34762  islshpat  34799  cmtfvalN  34992  cmtvalN  34993  ishlat1  35134  ishlat2  35135  3dim0  35238  2dim  35251  islvol5  35360  lhpexle3  35793  cdleme0ex2N  36006  cdleme0nex  36072  cdlemg2cex  36373  cdlemg33b0  36483  cdlemg33b  36489  cdlemg33c  36490  cdlemg33e  36492  dib1dim  36948  diblsmopel  36954  dihopelvalcpre  37031  lcfls1c  37319  3anrabdioph  37840  issdrg2  38262  fgraphxp  38283  dfrtrcl5  38430  brfvrcld2  38478  df3an2  38555  dfvd3  39301  3impexpVD  39582  rfcnnnub  39686  stoweidlem35  40747  smflimlem4  41480  ndmaovass  41784  nltle2tri  41825  elfz2z  41827  pfxccatin12lem2  41926  pfxccatin12  41927  pfxccat3a  41931  gboge9  42154  sbgoldbalt  42171  nnsum4primesodd  42186  nnsum4primesoddALTV  42187  bgoldbtbndlem4  42198  bgoldbtbnd  42199  ismhm0  42307  rnglz  42386  rngcsect  42482  rngcinv  42483  rngcsectALTV  42494  rngcinvALTV  42495  ringcsect  42533  ringcinv  42534  ringcsectALTV  42557  ringcinvALTV  42558  islindeps  42744  islindeps2  42774  isldepslvec2  42776  elbigo2  42848
  Copyright terms: Public domain W3C validator