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 1102
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 456. (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 1100 . 2 wff (𝜑𝜓𝜒)
51, 2wa 384 . . 3 wff (𝜑𝜓)
65, 3wa 384 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 197 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1109  3anan32  1111  3ancomaOLD  1113  3ancomb  1114  3anrotOLD  1117  3an4anass  1122  3anorOLD  1123  3ioran  1124  3ianor  1125  3impa  1129  3impOLD  1131  3expa  1140  3jca  1151  3simpaOLD  1172  3anbi123i  1187  3pm3.2i  1431  pm3.2an3OLD  1433  3anbi123d  1553  3anim123d  1560  an6  1562  an3andi  1599  an33rean  1600  cadan  1703  19.26-3an  1961  19.26-3anOLD  1962  nf3and  1989  nf3an  1993  4exdistr  2050  eeeanv  2357  nf3andOLD  2407  nf3anOLD  2413  sb3an  2559  mopick2  2704  r3al  3128  r19.26-3  3254  3reeanv  3296  ceqsex3v  3440  ceqsex4v  3441  ceqsex8v  3443  sbc3an  3691  elin3  4003  rexdifpr  4399  raltpg  4428  tpss  4556  opthprneg  4587  dfopif  4592  disjxun  4842  otth2  5141  otthg  5143  oteqex  5153  poirr  5243  po3nr  5246  wefrc  5305  rabxp  5354  brinxp2OLD  5381  f1orn  6359  fpropnf1  6744  dff1o6  6751  oprabid  6901  oprabv  6929  ndmovass  7048  elovmpt2  7105  elovmpt2rab  7106  elovmpt2rab1  7107  elovmpt3rab1  7119  dfwe2  7207  opiota  7457  dfxp3  7459  bropopvvv  7485  oaord  7860  oeeu  7916  nnaord  7932  swoso  8008  fiint  8472  funsnfsupp  8534  alephval3  9212  ingru  9918  axgroth3  9934  ltrelxr  10380  ltxrlt  10389  wloglei  10841  sup2  11260  rexuz2  11953  ltxr  12161  elixx3g  12402  ixxun  12405  elioo4g  12448  elioopnf  12482  elioomnf  12483  elicopnf  12484  elxrge0  12497  divelunit  12533  elfz2  12552  elfzuzb  12555  uzsplit  12631  fznn0  12651  elfzmlbp  12670  preduz  12681  elfzo2  12693  fzolb2  12697  fzouzsplit  12723  ssfzo12bi  12783  fzind2  12806  ccatsymb  13575  swrdsbslen  13668  swrdspsleq  13669  swrdccatin2  13707  swrdccatin12lem2  13709  swrdccatin12lem3  13710  swrdccatin12  13711  repsdf2  13745  repswsymball  13746  repswsymballbi  13747  repswswrd  13751  s3eq3seq  13904  wrdl3s3  13926  s3sndisj  13927  s3iunsndisj  13928  abs2dif  14291  sinltx  15135  divalglem8  15339  divalglem10  15341  divalgb  15343  bitsval2  15362  divgcdz  15448  rplpwr  15491  cncongr1  15595  pythagtriplem2  15735  pythagtrip  15752  prmgaplem4  15971  isstruct  16077  setsstruct2  16103  imasvscafn  16398  mreexmrid  16504  iscatd2  16542  issect  16613  issect2  16614  oppcsect  16638  isfunc  16724  funcpropd  16760  fucsect  16832  fucinv  16833  initoeu2  16866  setcsect  16939  setcinv  16940  issubm2  17549  issubg3  17810  resgrpisgrp  17813  cycsubgcl  17818  eqgval  17841  eqger  17842  isgim  17902  gaorb  17937  gaorber  17938  gastacos  17940  symg2bas  18015  galactghm  18020  gsmsymgreqlem2  18048  pmtr3ncom  18092  ispgp  18204  efgcpbllema  18364  efgcpbllemb  18365  eqgabl  18437  dprdw  18607  ringpropd  18780  ringrghm  18803  isirred2  18899  rim0to0  18942  drngid2  18963  islss  19135  islmim  19265  lmhmpropd  19276  isassa  19520  mpfrcl  19722  zndvds  20101  znleval  20106  znleval2  20107  obselocv  20278  matinvgcell  20447  mat1dimscm  20488  scmatscm  20526  scmatf1  20544  mdetunilem7  20631  cpmatacl  20730  cpmatmcl  20733  mat2pmatf1  20743  mat2pmatghm  20744  mat2pmatmul  20745  mat2pmatlin  20749  mat2pmatscmxcl  20754  m2pmfzgsumcl  20762  decpmataa0  20782  monmatcollpw  20793  pmatcollpwscmatlem1  20803  pmatcollpwscmatlem2  20804  pm2mpghm  20830  pm2mpmhmlem2  20833  monmat2matmon  20838  chfacfisf  20868  chfacfisfcpmat  20869  chfacfpmmulgsum2  20879  isbasis3g  20963  leordtvallem2  21225  lmfval  21246  lmbr  21272  lmbr2  21273  lmmo  21394  dfconn2  21432  ptbasin  21590  ptbasfi  21594  txcnpi  21621  ptcnp  21635  hausdiag  21658  qtophmeo  21830  fbunfip  21882  elflim2  21977  hausflimi  21993  isfcls  22022  isfcls2  22026  istmd  22087  istgp  22090  istrg  22176  istdrg  22178  istdrg2  22190  istlm  22197  imasdsf1olem  22387  xmeterval  22446  xmeter  22447  prdsxmslem2  22543  blval2  22576  isngp  22609  isngp2  22610  isngp3  22611  isnlm  22688  cnbl0  22786  cnblcld  22787  elii1  22943  isphtpc  23002  phtpcer  23003  isclmp  23105  iscph  23178  lmmbr  23264  lmmbr2  23265  lmmbrf  23268  iscfil2  23272  iscau3  23284  iscau4  23285  iscauf  23286  caucfil  23289  isbn  23343  ishl2  23374  ovolfcl  23443  ioombl1lem4  23538  mbfmax  23626  iblpos  23769  limcrcl  23848  ig1pval3  24144  ulmdvlem3  24366  ellogdm  24595  relogbcl  24721  fsumvma2  25149  chpchtsum  25154  chpub  25155  dchrelbas3  25173  gausslemma2dlem1a  25300  lnhl  25720  colopp  25871  dfcgra2  25931  axeuclidlem  26052  axeuclid  26053  edgupgr  26239  umgr2edg1  26314  subusgr  26393  nbgrel  26445  nb3grpr2  26497  nb3gr2nb  26498  isuvtx  26511  isuvtxaOLD  26512  nbupgruvtxres  26526  iscplgredg  26537  cplgr3v  26555  rusgrpropedg  26704  rgrusgrprc  26709  rusgrprc  26710  upgriswlk  26761  wlkonprop  26778  wksonproplem  26825  usgr2pth0  26885  isclwlke  26897  crctcshtrl  26940  iswwlksnx  26957  wwlknbp  26959  2trld  27074  rusgrnumwwlkl1  27106  rusgrnumwwlkb0  27109  rusgrnumwwlk  27113  clwlkclwwlkflem  27143  erclwwlkref  27159  clwwlkwwlksb  27200  erclwwlknref  27216  clwlksf1clwwlklem0OLD  27234  clwwlknonelOLD  27259  clwwlknon2x  27267  0wlk  27285  3spthd  27345  umgr3v3e3cycl  27353  frgr3v  27446  1to3vfriswmgr  27451  frgr2wwlkeu  27498  numclwwlk1lem2fo  27533  dlwwlknondlwlknonf1o  27541  nvex  27790  isnv  27791  dfadj2  29068  cnvadj  29075  adjeq  29118  eleigvec  29140  eleigvec2  29141  chirredi  29577  or3di  29631  dfrp2  29855  eliccelico  29862  omndmul2  30033  isorng  30120  pmtrprfv2  30169  fzto1st  30174  psgnfzto1st  30176  eulerpartlemv  30747  eulerpartlemd  30749  eulerpartlemn  30764  prob01  30796  probun  30802  bnj170  31085  bnj248  31087  bnj252  31090  bnj253  31091  bnj945  31162  bnj1098  31172  bnj1224  31190  bnj150  31264  bnj153  31268  bnj545  31283  bnj557  31289  bnj571  31294  bnj594  31300  bnj864  31310  bnj865  31311  bnj849  31313  bnj964  31331  bnj986  31342  bnj996  31343  bnj1033  31355  bnj1110  31368  bnj1128  31376  bnj1174  31389  pconnconn  31531  resconn  31546  iscvm  31559  cvmlift2lem12  31614  cvmlift3lem5  31623  elmpst  31751  mpstrcl  31756  lediv2aALT  31888  dfso3  31918  br6  31964  etasslt  32236  elfuns  32338  brimg  32360  brsuccf  32364  cgrxfr  32478  segcon2  32528  seglecgr12im  32533  seglecgr12  32534  segletr  32537  btwnoutside  32548  broutsideof3  32549  outsideoftr  32552  outsidele  32555  bj-imn3ani  32882  relowlpssretop  33523  lindsenlbs  33712  matunitlindflem2  33714  fdc  33847  isbnd3b  33890  ablo4pnp  33985  crngm4  34108  isidlc  34120  pridl  34142  ispridl2  34143  ispridlc  34175  ts3an1  34262  ts3an2  34263  ts3an3  34264  brres2  34347  eldmqsres  34363  xrninxp  34458  xrninxp2  34459  islshpsm  34755  islshpat  34792  cmtfvalN  34985  cmtvalN  34986  ishlat1  35127  ishlat2  35128  3dim0  35232  2dim  35245  islvol5  35354  lhpexle3  35787  cdleme0ex2N  35999  cdleme0nex  36065  cdlemg2cex  36366  cdlemg33b0  36476  cdlemg33b  36482  cdlemg33c  36483  cdlemg33e  36485  dib1dim  36940  diblsmopel  36946  dihopelvalcpre  37023  lcfls1c  37311  3anrabdioph  37842  issdrg2  38263  fgraphxp  38284  dfrtrcl5  38430  brfvrcld2  38478  df3an2  38555  dfvd3  39299  3impexpVD  39579  rfcnnnub  39683  stoweidlem35  40725  smflimlem4  41458  ndmaovass  41789  nltle2tri  41892  elfz2z  41894  pfxccatin12lem2  41993  pfxccatin12  41994  pfxccat3a  41998  gboge9  42221  sbgoldbalt  42238  nnsum4primesodd  42253  nnsum4primesoddALTV  42254  bgoldbtbndlem4  42265  bgoldbtbnd  42266  ismhm0  42367  rnglz  42446  rngcsect  42542  rngcinv  42543  rngcsectALTV  42554  rngcinvALTV  42555  ringcsect  42593  ringcinv  42594  ringcsectALTV  42617  ringcinvALTV  42618  islindeps  42804  islindeps2  42834  isldepslvec2  42836  elbigo2  42908
  Copyright terms: Public domain W3C validator