MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3an Structured version   Unicode version

Definition df-3an 984
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 653. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3an  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3w3a 982 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 370 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 370 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 187 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff setvar class
This definition is referenced by:  3anass  986  3anrot  987  3ancoma  989  3anan32  994  3anor  998  3ioran  1000  3simpa  1002  3pm3.2i  1183  pm3.2an3  1184  3jca  1185  3anbi123i  1194  3imp  1199  3an4anass  1229  3anbi123d  1335  3anim123d  1342  an6  1344  an3andi  1377  an33rean  1378  cadan  1505  19.26-3an  1728  4exdistr  1833  nf3and  1986  nf3an  1990  eeeanv  2048  sb3an  2198  mopick2  2339  r3al  2802  r19.26-3  2954  3reeanv  2994  ceqsex3v  3121  ceqsex4v  3122  ceqsex8v  3124  sbc3an  3357  elin3  3654  raltpg  4051  tpss  4165  dfopif  4184  disjxun  4421  otth2  4702  otthg  4704  oteqex  4713  poirr  4785  po3nr  4788  wefrc  4847  rabxp  4890  brinxp2  4915  brinxp  4916  f1orn  5841  dff1o6  6189  oprabid  6332  oprabv  6353  ndmovass  6471  elovmpt2  6528  elovmpt2rab  6529  elovmpt2rab1  6530  elovmpt3rab1  6541  dfwe2  6622  opiota  6866  dfxp3  6867  bropopvvv  6887  oaord  7259  oeeu  7315  nnaord  7331  swoso  7405  fiint  7857  funsnfsupp  7916  alephval3  8548  fpwwe2lem8  9069  fpwwe2lem9  9070  fpwwe2lem12  9073  ingru  9247  axgroth3  9263  ltrelxr  9702  ltxrlt  9711  wloglei  10153  sup2  10572  rexuz2  11217  ltxr  11422  elixx3g  11655  ixxun  11658  elioo4g  11702  elioopnf  11735  elioomnf  11736  elicopnf  11737  elxrge0  11748  divelunit  11781  elfz2  11798  elfzuzb  11801  uzsplit  11873  fznn0  11893  elfzmlbp  11909  preduz  11918  elfzo2  11930  fzolb2  11934  fzouzsplit  11960  ssfzo12bi  12012  fzind2  12029  ccatsymb  12731  swrdsbslen  12806  swrdspsleq  12807  swrdccatin2  12845  swrdccatin12lem2  12847  swrdccatin12lem3  12848  swrdccatin12  12849  repsdf2  12883  repswsymball  12884  repswsymballbi  12885  repswswrd  12889  abs2dif  13395  sinltx  14242  divalglem8  14379  divalglem10  14382  divalgb  14384  bitsval2  14397  rplpwr  14523  pythagtriplem2  14766  pythagtrip  14783  prmgaplem4  15023  pwsle  15389  imasvscafn  15442  mreexmrid  15548  iscatd2  15586  issect  15657  issect2  15658  oppcsect  15682  isfunc  15768  funcpropd  15804  fucsect  15876  fucinv  15877  initoeu2  15910  setcsect  15983  setcinv  15984  issubm2  16594  issubg3  16834  resgrpisgrp  16837  cycsubgcl  16842  eqgval  16865  eqger  16866  isgim  16925  gaorb  16960  gaorber  16961  gastacos  16963  symg2bas  17038  galactghm  17043  gsmsymgreqlem2  17071  pmtr3ncom  17115  ispgp  17243  efgcpbllema  17403  efgcpbllemb  17404  eqgabl  17474  dprdw  17641  ringpropd  17811  ringrghm  17832  isirred2  17928  rim0to0  17969  drngid2  17990  islss  18157  islmim  18284  lmhmpropd  18295  isassa  18538  mpfrcl  18740  zndvds  19118  znleval  19123  znleval2  19124  obselocv  19289  matinvgcell  19458  mat1dimscm  19498  scmatscm  19536  scmatf1  19554  mdetunilem7  19641  cpmatacl  19738  cpmatmcl  19741  mat2pmatf1  19751  mat2pmatghm  19752  mat2pmatmul  19753  mat2pmatlin  19757  mat2pmatscmxcl  19762  m2pmfzgsumcl  19770  decpmataa0  19790  monmatcollpw  19801  pmatcollpwscmatlem1  19811  pmatcollpwscmatlem2  19812  pm2mpghm  19838  pm2mpmhmlem2  19841  monmat2matmon  19846  chfacfisf  19876  chfacfisfcpmat  19877  chfacfpmmulgsum2  19887  isbasis3g  19962  leordtvallem2  20225  lmfval  20246  lmbr  20272  lmbr2  20273  lmmo  20394  dfcon2  20432  ptbasin  20590  ptbasfi  20594  txcnpi  20621  ptcnp  20635  hausdiag  20658  qtophmeo  20830  fbunfip  20882  elflim2  20977  hausflimi  20993  isfcls  21022  isfcls2  21026  istmd  21087  istgp  21090  istrg  21176  istdrg  21178  istdrg2  21190  istlm  21197  imasdsf1olem  21386  xmeterval  21445  xmeter  21446  prdsxmslem2  21542  blval2  21575  isngp  21608  isngp2  21609  isngp3  21610  isnlm  21676  cnbl0  21792  cnblcld  21793  elii1  21961  isphtpc  22023  phtpcer  22024  iscph  22146  lmmbr  22226  lmmbr2  22227  lmmbrf  22230  iscfil2  22234  iscau3  22246  iscau4  22247  iscauf  22248  caucfil  22251  isbn  22304  ishl2  22335  ovolfcl  22417  ioombl1lem4  22512  mbfmax  22603  iblpos  22748  limcrcl  22827  ig1pval3  23124  ig1pval3OLD  23130  ulmdvlem3  23355  ellogdm  23582  relogbcl  23708  fsumvma2  24140  chpchtsum  24145  chpub  24146  dchrelbas3  24164  lnhl  24658  colopp  24809  dfcgra2  24869  axeuclidlem  24990  axeuclid  24991  nb3grapr2  25180  nb3gra2nb  25181  0wlk  25273  0trl  25274  constr2wlk  25326  3v3e3cycl1  25370  wwlknred  25449  wwlknndef  25463  isclwlk  25482  clwwlkprop  25496  clwwlknndef  25499  clwwlknwwlkncl  25526  wwlkext2clwwlk  25529  wwlksubclwwlk  25530  clwwnisshclwwn  25535  erclwwlkref  25539  erclwwlknref  25551  clwlkfoclwwlk  25571  el2wlkonotot0  25598  el2wlkonotot  25599  el2wlkonotot1  25600  2wlkonotv  25603  usg2spthonot0  25615  cusgraisrusgra  25664  rusgranumwlkl1  25673  rusgranumwlkb0  25679  rusgra0edg  25681  rusgranumwlk  25683  frgra3v  25728  1to3vfriswmgra  25733  frgraregorufrg  25798  extwwlkfablem2  25804  numclwwlkffin  25808  numclwwlkovfel2  25809  numclwwlkovf2  25810  numclwwlkovf2ex  25812  numclwwlkovgelim  25815  numclwlk1lem2fo  25821  numclwwlk2lem1  25828  numclwwlk7  25840  nvex  26228  isnv  26229  dfadj2  27536  cnvadj  27543  adjeq  27586  eleigvec  27608  eleigvec2  27609  chirredi  28045  or3di  28099  dfrp2  28358  eliccelico  28365  omndmul2  28482  isorng  28570  pmtrprfv2  28619  fzto1st  28624  psgnfzto1st  28626  eulerpartlemv  29205  eulerpartlemd  29207  eulerpartlemn  29222  prob01  29254  probun  29260  bnj170  29511  bnj248  29513  bnj252  29516  bnj253  29517  bnj945  29593  bnj1098  29603  bnj1224  29621  bnj150  29695  bnj153  29699  bnj545  29714  bnj557  29720  bnj571  29725  bnj594  29731  bnj864  29741  bnj865  29742  bnj849  29744  bnj964  29762  bnj986  29773  bnj996  29774  bnj1033  29786  bnj1110  29799  bnj1128  29807  bnj1174  29820  pconcon  29962  rescon  29977  iscvm  29990  cvmlift2lem12  30045  cvmlift3lem5  30054  elmpst  30182  mpstrcl  30187  lediv2aALT  30329  dfso3  30360  br6  30404  nofulllem2  30597  nofulllem5  30600  elfuns  30687  brimg  30709  brsuccf  30713  cgrxfr  30827  segcon2  30877  seglecgr12im  30882  seglecgr12  30883  segletr  30886  btwnoutside  30897  broutsideof3  30898  outsideoftr  30901  outsidele  30904  bj-imn3ani  31175  relowlpssretop  31731  fdc  32038  isbnd3b  32081  ablo4pnp  32142  crngm4  32200  isidlc  32212  pridl  32234  ispridl2  32235  ispridlc  32267  ts3an1  32356  ts3an2  32357  ts3an3  32358  islshpsm  32515  islshpat  32552  cmtfvalN  32745  cmtvalN  32746  ishlat1  32887  ishlat2  32888  3dim0  32991  2dim  33004  islvol5  33113  lhpexle3  33546  cdleme0ex2N  33759  cdleme0nex  33825  cdlemg2cex  34127  cdlemg33b0  34237  cdlemg33b  34243  cdlemg33c  34244  cdlemg33e  34246  dib1dim  34702  diblsmopel  34708  dihopelvalcpre  34785  lcfls1c  35073  3anrabdioph  35594  issdrg2  36034  fgraphxp  36058  dfrtrcl5  36206  brfvrcld2  36254  df3an2  36331  dfvd3  36932  3impexpVD  37225  rfcnnnub  37330  stoweidlem35  37836  ndmaovass  38578  nltle2tri  38586  gboage9  38735  sgoldbalt  38752  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  bgoldbtbndlem4  38773  bgoldbtbnd  38774  pfxccatin12lem2  38835  pfxccatin12  38836  pfxccat3a  38840  rexdifpr  38860  elfz2z  38909  edgumgra  39043  usgr2edg1  39076  subusgr  39133  nb3grpr2  39217  nb3gr2nb  39218  isuvtxa  39226  nbumgruvtxres  39237  iscplgredg  39242  cplgr3v  39259  usgra2pth0  39289  ismhm0  39425  rnglz  39504  rngcsect  39602  rngcinv  39603  rngcsectALTV  39614  rngcinvALTV  39615  ringcsect  39653  ringcinv  39654  ringcsectALTV  39677  ringcinvALTV  39678  islindeps  39868  islindeps2  39898  isldepslvec2  39900  elbigo2  39985
  Copyright terms: Public domain W3C validator