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  1507  19.26-3an  1729  4exdistr  1832  nf3and  1984  nf3an  1988  eeeanv  2046  sb3an  2195  mopick2  2340  r3al  2812  r19.26-3  2964  3reeanv  3004  ceqsex3v  3127  ceqsex4v  3128  ceqsex8v  3130  sbc3an  3363  elin3  3660  raltpg  4054  tpss  4168  dfopif  4187  disjxun  4424  otth2  4703  otthg  4705  oteqex  4714  poirr  4786  po3nr  4789  wefrc  4848  rabxp  4891  brinxp2  4916  brinxp  4917  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  7256  oeeu  7312  nnaord  7328  swoso  7402  fiint  7854  funsnfsupp  7913  alephval3  8539  fpwwe2lem8  9061  fpwwe2lem9  9062  fpwwe2lem12  9065  ingru  9239  axgroth3  9255  ltrelxr  9694  ltxrlt  9703  wloglei  10145  sup2  10565  rexuz2  11210  ltxr  11415  elixx3g  11648  ixxun  11651  elioo4g  11695  elioopnf  11728  elioomnf  11729  elicopnf  11730  elxrge0  11739  divelunit  11772  elfz2  11789  elfzuzb  11792  uzsplit  11864  fznn0  11884  elfzmlbp  11900  preduz  11909  elfzo2  11921  fzolb2  11925  fzouzsplit  11951  ssfzo12bi  12003  fzind2  12020  ccatsymb  12714  swrdsbslen  12789  swrdspsleq  12790  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12lem3  12831  swrdccatin12  12832  repsdf2  12866  repswsymball  12867  repswsymballbi  12868  repswswrd  12872  abs2dif  13374  sinltx  14221  divalglem8  14356  divalglem10  14358  divalgb  14360  bitsval2  14373  rplpwr  14495  pythagtriplem2  14730  pythagtrip  14747  prmgaplem4  14987  pwsle  15349  imasvscafn  15394  mreexmrid  15500  iscatd2  15538  issect  15609  issect2  15610  oppcsect  15634  isfunc  15720  funcpropd  15756  fucsect  15828  fucinv  15829  initoeu2  15862  setcsect  15935  setcinv  15936  issubm2  16546  issubg3  16786  resgrpisgrp  16789  cycsubgcl  16794  eqgval  16817  eqger  16818  isgim  16877  gaorb  16912  gaorber  16913  gastacos  16915  symg2bas  16990  galactghm  16995  gsmsymgreqlem2  17023  pmtr3ncom  17067  ispgp  17179  efgcpbllema  17339  efgcpbllemb  17340  eqgabl  17410  dprdw  17577  ringpropd  17747  ringrghm  17768  isirred2  17864  rim0to0  17905  drngid2  17926  islss  18093  islmim  18220  lmhmpropd  18231  isassa  18474  mpfrcl  18676  zndvds  19051  znleval  19056  znleval2  19057  obselocv  19222  matinvgcell  19391  mat1dimscm  19431  scmatscm  19469  scmatf1  19487  mdetunilem7  19574  cpmatacl  19671  cpmatmcl  19674  mat2pmatf1  19684  mat2pmatghm  19685  mat2pmatmul  19686  mat2pmatlin  19690  mat2pmatscmxcl  19695  m2pmfzgsumcl  19703  decpmataa0  19723  monmatcollpw  19734  pmatcollpwscmatlem1  19744  pmatcollpwscmatlem2  19745  pm2mpghm  19771  pm2mpmhmlem2  19774  monmat2matmon  19779  chfacfisf  19809  chfacfisfcpmat  19810  chfacfpmmulgsum2  19820  isbasis3g  19895  leordtvallem2  20158  lmfval  20179  lmbr  20205  lmbr2  20206  lmmo  20327  dfcon2  20365  ptbasin  20523  ptbasfi  20527  txcnpi  20554  ptcnp  20568  hausdiag  20591  qtophmeo  20763  fbunfip  20815  elflim2  20910  hausflimi  20926  isfcls  20955  isfcls2  20959  istmd  21020  istgp  21023  istrg  21109  istdrg  21111  istdrg2  21123  istlm  21130  imasdsf1olem  21319  xmeterval  21378  xmeter  21379  prdsxmslem2  21475  blval2  21508  isngp  21541  isngp2  21542  isngp3  21543  isnlm  21609  cnbl0  21705  cnblcld  21706  elii1  21859  isphtpc  21918  phtpcer  21919  iscph  22041  lmmbr  22121  lmmbr2  22122  lmmbrf  22125  iscfil2  22129  iscau3  22141  iscau4  22142  iscauf  22143  caucfil  22146  isbn  22199  ishl2  22230  ovolfcl  22298  ioombl1lem4  22391  mbfmax  22482  iblpos  22627  limcrcl  22706  ig1pval3  23000  ulmdvlem3  23222  ellogdm  23449  relogbcl  23575  fsumvma2  24005  chpchtsum  24010  chpub  24011  dchrelbas3  24029  colopp  24667  dfcgra2  24726  axeuclidlem  24838  axeuclid  24839  nb3grapr2  25027  nb3gra2nb  25028  0wlk  25120  0trl  25121  constr2wlk  25173  3v3e3cycl1  25217  wwlknred  25296  wwlknndef  25310  isclwlk  25329  clwwlkprop  25343  clwwlknndef  25346  clwwlknwwlkncl  25373  wwlkext2clwwlk  25376  wwlksubclwwlk  25377  clwwnisshclwwn  25382  erclwwlkref  25386  erclwwlknref  25398  clwlkfoclwwlk  25418  el2wlkonotot0  25445  el2wlkonotot  25446  el2wlkonotot1  25447  2wlkonotv  25450  usg2spthonot0  25462  cusgraisrusgra  25511  rusgranumwlkl1  25520  rusgranumwlkb0  25526  rusgra0edg  25528  rusgranumwlk  25530  frgra3v  25575  1to3vfriswmgra  25580  frgraregorufrg  25645  extwwlkfablem2  25651  numclwwlkffin  25655  numclwwlkovfel2  25656  numclwwlkovf2  25657  numclwwlkovf2ex  25659  numclwwlkovgelim  25662  numclwlk1lem2fo  25668  numclwwlk2lem1  25675  numclwwlk7  25687  nvex  26075  isnv  26076  dfadj2  27373  cnvadj  27380  adjeq  27423  eleigvec  27445  eleigvec2  27446  chirredi  27882  or3di  27936  dfrp2  28188  eliccelico  28195  omndmul2  28313  isorng  28401  pmtrprfv2  28450  fzto1st  28455  psgnfzto1st  28457  eulerpartlemv  29023  eulerpartlemd  29025  eulerpartlemn  29040  prob01  29072  probun  29078  bnj170  29291  bnj248  29293  bnj252  29296  bnj253  29297  bnj945  29373  bnj1098  29383  bnj1224  29401  bnj150  29475  bnj153  29479  bnj545  29494  bnj557  29500  bnj571  29505  bnj594  29511  bnj864  29521  bnj865  29522  bnj849  29524  bnj964  29542  bnj986  29553  bnj996  29554  bnj1033  29566  bnj1110  29579  bnj1128  29587  bnj1174  29600  pconcon  29742  rescon  29757  iscvm  29770  cvmlift2lem12  29825  cvmlift3lem5  29834  elmpst  29962  mpstrcl  29967  lediv2aALT  30109  dfso3  30140  br6  30184  nofulllem2  30377  nofulllem5  30380  elfuns  30467  brimg  30489  brsuccf  30493  cgrxfr  30607  segcon2  30657  seglecgr12im  30662  seglecgr12  30663  segletr  30666  btwnoutside  30677  broutsideof3  30678  outsideoftr  30681  outsidele  30684  bj-imn3ani  30955  relowlpssretop  31501  fdc  31778  isbnd3b  31821  ablo4pnp  31882  crngm4  31940  isidlc  31952  pridl  31974  ispridl2  31975  ispridlc  32007  ts3an1  32096  ts3an2  32097  ts3an3  32098  islshpsm  32255  islshpat  32292  cmtfvalN  32485  cmtvalN  32486  ishlat1  32627  ishlat2  32628  3dim0  32731  2dim  32744  islvol5  32853  lhpexle3  33286  cdleme0ex2N  33499  cdleme0nex  33565  cdlemg2cex  33867  cdlemg33b0  33977  cdlemg33b  33983  cdlemg33c  33984  cdlemg33e  33986  dib1dim  34442  diblsmopel  34448  dihopelvalcpre  34525  lcfls1c  34813  3anrabdioph  35334  issdrg2  35763  fgraphxp  35787  brfvrcld2  35923  dfvd3  36599  3impexpVD  36892  rfcnnnub  36997  stoweidlem35  37465  ndmaovass  38098  nltle2tri  38106  gboage9  38255  sgoldbalt  38272  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  bgoldbtbndlem4  38293  bgoldbtbnd  38294  pfxccatin12lem2  38355  pfxccatin12  38356  pfxccat3a  38360  rexdifpr  38377  elfz2z  38404  usgra2pth0  38425  ismhm0  38563  rnglz  38642  rngcsect  38740  rngcinv  38741  rngcsectALTV  38752  rngcinvALTV  38753  ringcsect  38791  ringcinv  38792  ringcsectALTV  38815  ringcinvALTV  38816  islindeps  39006  islindeps2  39036  isldepslvec2  39038  elbigo2  39124
  Copyright terms: Public domain W3C validator