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

Definition df-3an 976
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 649. (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 974 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 369 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 369 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 184 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff setvar class
This definition is referenced by:  3anass  978  3anrot  979  3ancoma  981  3anan32  986  3anor  990  3ioran  992  3simpa  994  3pm3.2i  1175  pm3.2an3  1176  3jca  1177  3anbi123i  1186  3imp  1191  3an4anass  1220  3anbi123d  1300  3anim123d  1307  an6  1309  an3andi  1342  an33rean  1343  cadan  1447  19.26-3an  1669  4exdistr  1767  nf3and  1912  nf3an  1916  eeeanv  1975  sb3an  2127  mopick2  2348  r3al  2823  r19.26-3  2972  3reeanv  3012  ceqsex3v  3135  ceqsex4v  3136  ceqsex8v  3138  sbc3an  3376  elin3  3675  raltpg  4065  tpss  4180  dfopif  4199  disjxun  4435  otth2  4718  otthg  4720  oteqex  4730  poirr  4801  po3nr  4804  wefrc  4863  rabxp  5026  brinxp2  5051  brinxp  5052  f1orn  5816  dff1o6  6166  oprabid  6308  oprabv  6330  ndmovass  6448  elovmpt2  6505  elovmpt2rab  6506  elovmpt2rab1  6507  elovmpt3rab1  6521  dfwe2  6602  opiota  6844  dfxp3  6845  bropopvvv  6865  oaord  7198  oeeu  7254  nnaord  7270  swoso  7344  fiint  7799  funsnfsupp  7855  alephval3  8494  fpwwe2lem8  9018  fpwwe2lem9  9019  fpwwe2lem12  9022  ingru  9196  axgroth3  9212  ltrelxr  9651  ltxrlt  9658  wloglei  10092  sup2  10506  rexuz2  11143  ltxr  11335  elixx3g  11553  ixxun  11556  elioo4g  11596  elioopnf  11629  elioomnf  11630  elicopnf  11631  elxrge0  11640  divelunit  11673  elfz2  11690  elfzuzb  11693  uzsplit  11761  fznn0  11781  elfzmlbp  11797  elfzo2  11814  fzolb2  11817  fzouzsplit  11842  ssfzo12bi  11889  fzind2  11906  ccatsymb  12582  swrdccatin2  12694  swrdccatin12lem2  12696  swrdccatin12lem3  12697  swrdccatin12  12698  repsdf2  12732  repswsymball  12733  repswsymballbi  12734  repswswrd  12738  abs2dif  13147  sinltx  13906  divalglem8  14040  divalglem10  14042  divalgb  14044  bitsval2  14057  rplpwr  14176  pythagtriplem2  14323  pythagtrip  14340  pwsle  14871  imasvscafn  14916  mreexmrid  15022  iscatd2  15060  issect  15130  issect2  15131  oppcsect  15150  isfunc  15212  funcpropd  15248  fucsect  15320  fucinv  15321  setcsect  15395  setcinv  15396  issubm2  15958  issubg3  16198  resgrpisgrp  16201  cycsubgcl  16206  eqgval  16229  eqger  16230  isgim  16289  gaorb  16324  gaorber  16325  gastacos  16327  symg2bas  16402  galactghm  16407  gsmsymgreqlem2  16435  pmtr3ncom  16479  ispgp  16591  efgcpbllema  16751  efgcpbllemb  16752  eqgabl  16822  dprdw  17022  dprdwOLD  17029  ringpropd  17209  ringrghm  17230  isirred2  17329  rim0to0  17370  drngid2  17391  islss  17560  islmim  17687  lmhmpropd  17698  isassa  17943  mpfrcl  18166  zndvds  18566  znleval  18571  znleval2  18572  obselocv  18737  matinvgcell  18915  mat1dimscm  18955  scmatscm  18993  scmatf1  19011  mdetunilem7  19098  cpmatacl  19195  cpmatmcl  19198  mat2pmatf1  19208  mat2pmatghm  19209  mat2pmatmul  19210  mat2pmatlin  19214  mat2pmatscmxcl  19219  m2pmfzgsumcl  19227  decpmataa0  19247  monmatcollpw  19258  pmatcollpwscmatlem1  19268  pmatcollpwscmatlem2  19269  pm2mpghm  19295  pm2mpmhmlem2  19298  monmat2matmon  19303  chfacfisf  19333  chfacfisfcpmat  19334  chfacfpmmulgsum2  19344  isbasis3g  19428  leordtvallem2  19690  lmfval  19711  lmbr  19737  lmbr2  19738  lmmo  19859  dfcon2  19898  ptbasin  20056  ptbasfi  20060  txcnpi  20087  ptcnp  20101  hausdiag  20124  qtophmeo  20296  fbunfip  20348  elflim2  20443  hausflimi  20459  isfcls  20488  isfcls2  20492  istmd  20551  istgp  20554  istrg  20644  istdrg  20646  istdrg2  20658  istlm  20665  imasdsf1olem  20854  xmeterval  20913  xmeter  20914  prdsxmslem2  21010  blval2  21056  isngp  21094  isngp2  21095  isngp3  21096  isnlm  21162  cnbl0  21259  cnblcld  21260  elii1  21413  isphtpc  21472  phtpcer  21473  iscph  21595  lmmbr  21675  lmmbr2  21676  lmmbrf  21679  iscfil2  21683  iscau3  21695  iscau4  21696  iscauf  21697  caucfil  21700  isbn  21755  ishl2  21788  ovolfcl  21856  ioombl1lem4  21949  mbfmax  22034  iblpos  22177  limcrcl  22256  ig1pval3  22553  ulmdvlem3  22775  ellogdm  22998  fsumvma2  23467  chpchtsum  23472  chpub  23473  dchrelbas3  23491  axeuclidlem  24243  axeuclid  24244  nb3grapr2  24432  nb3gra2nb  24433  0wlk  24525  0trl  24526  constr2wlk  24578  3v3e3cycl1  24622  wwlknred  24701  wwlknndef  24715  isclwlk  24734  clwwlkprop  24748  clwwlknndef  24751  clwwlknwwlkncl  24778  wwlkext2clwwlk  24781  wwlksubclwwlk  24782  clwwnisshclwwn  24787  erclwwlkref  24791  erclwwlknref  24803  clwlkfoclwwlk  24823  el2wlkonotot0  24850  el2wlkonotot  24851  el2wlkonotot1  24852  2wlkonotv  24855  usg2spthonot0  24867  cusgraisrusgra  24916  rusgranumwlkl1  24925  rusgranumwlkb0  24931  rusgra0edg  24933  rusgranumwlk  24935  frgra3v  24980  1to3vfriswmgra  24985  frgraregorufrg  25050  extwwlkfablem2  25056  numclwwlkffin  25060  numclwwlkovfel2  25061  numclwwlkovf2  25062  numclwwlkovf2ex  25064  numclwwlkovgelim  25067  numclwlk1lem2fo  25073  numclwwlk2lem1  25080  numclwwlk7  25092  nvex  25482  isnv  25483  dfadj2  26782  cnvadj  26789  adjeq  26832  eleigvec  26854  eleigvec2  26855  chirredi  27291  or3di  27345  eliccelico  27566  omndmul2  27680  isorng  27767  relogbcl  27996  eulerpartlemv  28281  eulerpartlemd  28283  eulerpartlemn  28298  prob01  28330  probun  28336  pconcon  28654  rescon  28669  iscvm  28682  cvmlift2lem12  28737  cvmlift3lem5  28746  elmpst  28874  mpstrcl  28879  lediv2aALT  29021  dfso3  29075  br6  29162  preduz  29256  nofulllem2  29439  nofulllem5  29442  elfuns  29541  brimg  29563  brsuccf  29567  cgrxfr  29681  segcon2  29731  seglecgr12im  29736  seglecgr12  29737  segletr  29740  btwnoutside  29751  broutsideof3  29752  outsideoftr  29755  outsidele  29758  fdc  30214  isbnd3b  30257  ablo4pnp  30318  crngm4  30376  isidlc  30388  pridl  30410  ispridl2  30411  ispridlc  30443  ts3an1  30533  ts3an2  30534  ts3an3  30535  3anrabdioph  30692  issdrg2  31123  fgraphxp  31147  rfcnnnub  31365  stoweidlem35  31771  ndmaovass  32245  rexdifpr  32254  elfz2z  32285  usgra2pth0  32309  rngcsect  32663  rngcinv  32664  rngcsectOLD  32675  rngcinvOLD  32676  ringcsect  32711  ringcinv  32712  ringcsectOLD  32735  ringcinvOLD  32736  islindeps  32924  islindeps2  32954  isldepslvec2  32956  dfvd3  33236  3impexpVD  33524  bnj170  33618  bnj248  33620  bnj252  33623  bnj253  33624  bnj945  33700  bnj1098  33710  bnj1224  33728  bnj150  33802  bnj153  33806  bnj545  33821  bnj557  33827  bnj571  33832  bnj594  33838  bnj864  33848  bnj865  33849  bnj849  33851  bnj964  33869  bnj986  33880  bnj996  33881  bnj1033  33893  bnj1110  33906  bnj1128  33914  bnj1174  33927  bj-imn3ani  34059  islshpsm  34580  islshpat  34617  cmtfvalN  34810  cmtvalN  34811  ishlat1  34952  ishlat2  34953  3dim0  35056  2dim  35069  islvol5  35178  lhpexle3  35611  cdleme0ex2N  35824  cdleme0nex  35890  cdlemg2cex  36192  cdlemg33b0  36302  cdlemg33b  36308  cdlemg33c  36309  cdlemg33e  36311  dib1dim  36767  diblsmopel  36773  dihopelvalcpre  36850  lcfls1c  37138
  Copyright terms: Public domain W3C validator