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

Definition df-3an 993
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 659. (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 991 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 375 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 375 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 189 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff setvar class
This definition is referenced by:  3anass  995  3anrot  996  3ancoma  998  3anan32  1003  3anor  1007  3ioran  1009  3simpa  1011  3pm3.2i  1192  pm3.2an3  1193  3jca  1194  3anbi123i  1203  3imp  1208  3an4anass  1241  3anbi123d  1348  3anim123d  1355  an6  1357  an3andi  1392  an33rean  1393  cadan  1523  19.26-3an  1745  4exdistr  1851  nf3and  2020  nf3an  2024  eeeanv  2090  sb3an  2240  mopick2  2380  r3al  2780  r19.26-3  2931  3reeanv  2971  ceqsex3v  3100  ceqsex4v  3101  ceqsex8v  3103  sbc3an  3337  elin3  3636  raltpg  4035  tpss  4150  dfopif  4177  disjxun  4416  otth2  4700  otthg  4702  oteqex  4711  poirr  4788  po3nr  4791  wefrc  4850  rabxp  4893  brinxp2  4918  brinxp  4919  f1orn  5851  dff1o6  6204  oprabid  6347  oprabv  6371  ndmovass  6489  elovmpt2  6546  elovmpt2rab  6547  elovmpt2rab1  6548  elovmpt3rab1  6559  dfwe2  6640  opiota  6884  dfxp3  6885  bropopvvv  6906  oaord  7279  oeeu  7335  nnaord  7351  swoso  7425  fiint  7879  funsnfsupp  7938  alephval3  8572  fpwwe2lem8  9093  fpwwe2lem9  9094  fpwwe2lem12  9097  ingru  9271  axgroth3  9287  ltrelxr  9726  ltxrlt  9735  wloglei  10179  sup2  10598  rexuz2  11244  ltxr  11449  elixx3g  11682  ixxun  11685  elioo4g  11729  elioopnf  11762  elioomnf  11763  elicopnf  11764  elxrge0  11776  divelunit  11809  elfz2  11826  elfzuzb  11829  uzsplit  11901  fznn0  11921  elfzmlbp  11938  preduz  11948  elfzo2  11960  fzolb2  11964  fzouzsplit  11990  ssfzo12bi  12043  fzind2  12060  ccatsymb  12769  swrdsbslen  12847  swrdspsleq  12848  swrdccatin2  12886  swrdccatin12lem2  12888  swrdccatin12lem3  12889  swrdccatin12  12890  repsdf2  12924  repswsymball  12925  repswsymballbi  12926  repswswrd  12930  abs2dif  13450  sinltx  14298  divalglem8  14435  divalglem10  14438  divalgb  14440  bitsval2  14453  rplpwr  14579  pythagtriplem2  14822  pythagtrip  14839  prmgaplem4  15079  pwsle  15445  imasvscafn  15498  mreexmrid  15604  iscatd2  15642  issect  15713  issect2  15714  oppcsect  15738  isfunc  15824  funcpropd  15860  fucsect  15932  fucinv  15933  initoeu2  15966  setcsect  16039  setcinv  16040  issubm2  16650  issubg3  16890  resgrpisgrp  16893  cycsubgcl  16898  eqgval  16921  eqger  16922  isgim  16981  gaorb  17016  gaorber  17017  gastacos  17019  symg2bas  17094  galactghm  17099  gsmsymgreqlem2  17127  pmtr3ncom  17171  ispgp  17299  efgcpbllema  17459  efgcpbllemb  17460  eqgabl  17530  dprdw  17697  ringpropd  17867  ringrghm  17888  isirred2  17984  rim0to0  18025  drngid2  18046  islss  18213  islmim  18340  lmhmpropd  18351  isassa  18594  mpfrcl  18796  zndvds  19175  znleval  19180  znleval2  19181  obselocv  19346  matinvgcell  19515  mat1dimscm  19555  scmatscm  19593  scmatf1  19611  mdetunilem7  19698  cpmatacl  19795  cpmatmcl  19798  mat2pmatf1  19808  mat2pmatghm  19809  mat2pmatmul  19810  mat2pmatlin  19814  mat2pmatscmxcl  19819  m2pmfzgsumcl  19827  decpmataa0  19847  monmatcollpw  19858  pmatcollpwscmatlem1  19868  pmatcollpwscmatlem2  19869  pm2mpghm  19895  pm2mpmhmlem2  19898  monmat2matmon  19903  chfacfisf  19933  chfacfisfcpmat  19934  chfacfpmmulgsum2  19944  isbasis3g  20019  leordtvallem2  20282  lmfval  20303  lmbr  20329  lmbr2  20330  lmmo  20451  dfcon2  20489  ptbasin  20647  ptbasfi  20651  txcnpi  20678  ptcnp  20692  hausdiag  20715  qtophmeo  20887  fbunfip  20939  elflim2  21034  hausflimi  21050  isfcls  21079  isfcls2  21083  istmd  21144  istgp  21147  istrg  21233  istdrg  21235  istdrg2  21247  istlm  21254  imasdsf1olem  21443  xmeterval  21502  xmeter  21503  prdsxmslem2  21599  blval2  21632  isngp  21665  isngp2  21666  isngp3  21667  isnlm  21733  cnbl0  21849  cnblcld  21850  elii1  22018  isphtpc  22080  phtpcer  22081  iscph  22203  lmmbr  22283  lmmbr2  22284  lmmbrf  22287  iscfil2  22291  iscau3  22303  iscau4  22304  iscauf  22305  caucfil  22308  isbn  22361  ishl2  22392  ovolfcl  22474  ioombl1lem4  22570  mbfmax  22661  iblpos  22806  limcrcl  22885  ig1pval3  23182  ig1pval3OLD  23188  ulmdvlem3  23413  ellogdm  23640  relogbcl  23766  fsumvma2  24198  chpchtsum  24203  chpub  24204  dchrelbas3  24222  lnhl  24716  colopp  24867  dfcgra2  24927  axeuclidlem  25048  axeuclid  25049  nb3grapr2  25238  nb3gra2nb  25239  0wlk  25331  0trl  25332  constr2wlk  25384  3v3e3cycl1  25428  wwlknred  25507  wwlknndef  25521  isclwlk  25540  clwwlkprop  25554  clwwlknndef  25557  clwwlknwwlkncl  25584  wwlkext2clwwlk  25587  wwlksubclwwlk  25588  clwwnisshclwwn  25593  erclwwlkref  25597  erclwwlknref  25609  clwlkfoclwwlk  25629  el2wlkonotot0  25656  el2wlkonotot  25657  el2wlkonotot1  25658  2wlkonotv  25661  usg2spthonot0  25673  cusgraisrusgra  25722  rusgranumwlkl1  25731  rusgranumwlkb0  25737  rusgra0edg  25739  rusgranumwlk  25741  frgra3v  25786  1to3vfriswmgra  25791  frgraregorufrg  25856  extwwlkfablem2  25862  numclwwlkffin  25866  numclwwlkovfel2  25867  numclwwlkovf2  25868  numclwwlkovf2ex  25870  numclwwlkovgelim  25873  numclwlk1lem2fo  25879  numclwwlk2lem1  25886  numclwwlk7  25898  nvex  26286  isnv  26287  dfadj2  27594  cnvadj  27601  adjeq  27644  eleigvec  27666  eleigvec2  27667  chirredi  28103  or3di  28157  dfrp2  28404  eliccelico  28411  omndmul2  28526  isorng  28613  pmtrprfv2  28662  fzto1st  28667  psgnfzto1st  28669  eulerpartlemv  29247  eulerpartlemd  29249  eulerpartlemn  29264  prob01  29296  probun  29302  bnj170  29553  bnj248  29555  bnj252  29558  bnj253  29559  bnj945  29635  bnj1098  29645  bnj1224  29663  bnj150  29737  bnj153  29741  bnj545  29756  bnj557  29762  bnj571  29767  bnj594  29773  bnj864  29783  bnj865  29784  bnj849  29786  bnj964  29804  bnj986  29815  bnj996  29816  bnj1033  29828  bnj1110  29841  bnj1128  29849  bnj1174  29862  pconcon  30004  rescon  30019  iscvm  30032  cvmlift2lem12  30087  cvmlift3lem5  30096  elmpst  30224  mpstrcl  30229  lediv2aALT  30371  dfso3  30402  br6  30447  nofulllem2  30642  nofulllem5  30645  elfuns  30732  brimg  30754  brsuccf  30758  cgrxfr  30872  segcon2  30922  seglecgr12im  30927  seglecgr12  30928  segletr  30931  btwnoutside  30942  broutsideof3  30943  outsideoftr  30946  outsidele  30949  bj-imn3ani  31217  relowlpssretop  31813  fdc  32120  isbnd3b  32163  ablo4pnp  32224  crngm4  32282  isidlc  32294  pridl  32316  ispridl2  32317  ispridlc  32349  ts3an1  32438  ts3an2  32439  ts3an3  32440  islshpsm  32592  islshpat  32629  cmtfvalN  32822  cmtvalN  32823  ishlat1  32964  ishlat2  32965  3dim0  33068  2dim  33081  islvol5  33190  lhpexle3  33623  cdleme0ex2N  33836  cdleme0nex  33902  cdlemg2cex  34204  cdlemg33b0  34314  cdlemg33b  34320  cdlemg33c  34321  cdlemg33e  34323  dib1dim  34779  diblsmopel  34785  dihopelvalcpre  34862  lcfls1c  35150  3anrabdioph  35671  issdrg2  36110  fgraphxp  36134  dfrtrcl5  36282  brfvrcld2  36330  df3an2  36407  dfvd3  37005  3impexpVD  37293  rfcnnnub  37398  stoweidlem35  37997  ndmaovass  38843  nltle2tri  38851  gboage9  39000  sgoldbalt  39017  nnsum4primesodd  39026  nnsum4primesoddALTV  39027  bgoldbtbndlem4  39038  bgoldbtbnd  39039  pfxccatin12lem2  39102  pfxccatin12  39103  pfxccat3a  39107  rexdifpr  39131  fpropnf1  39174  elfz2z  39193  edgupgr  39369  usgr2edg1  39438  subusgr  39507  nb3grpr2  39603  nb3gr2nb  39604  isuvtxa  39613  nbupgruvtxres  39626  iscplgredg  39631  cplgr3v  39648  rusgrpropedg  39746  rgrusgrprc  39750  rusgrprc  39751  wlkOnprop  39805  lfgriswlk  39819  1wlksonproplem  39836  isclWlke  39900  01wlk  39928  2trld  39983  3spthd  40013  umgr3v3e3cycl  40021  usgra2pth0  40038  ismhm0  40174  rnglz  40253  rngcsect  40351  rngcinv  40352  rngcsectALTV  40363  rngcinvALTV  40364  ringcsect  40402  ringcinv  40403  ringcsectALTV  40426  ringcinvALTV  40427  islindeps  40615  islindeps2  40645  isldepslvec2  40647  elbigo2  40732
  Copyright terms: Public domain W3C validator