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

Definition df-3an 970
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 968 . 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  972  3anrot  973  3ancoma  975  3anan32  980  3anor  984  3ioran  986  3simpa  988  3pm3.2i  1169  pm3.2an3  1170  3jca  1171  3anbi123i  1180  3imp  1185  3an4anass  1214  3anbi123d  1294  3anim123d  1301  an6  1303  an3andi  1336  an33rean  1337  cadan  1438  cadanOLD  1439  19.26-3an  1654  nf3and  1868  nf3an  1872  4exdistr  1950  eeeanv  1953  sb3an  2110  mopick2  2365  r3al  2839  r19.26-3  2986  3reeanv  3025  ceqsex3v  3148  ceqsex4v  3149  ceqsex8v  3151  sbc3an  3389  elin3  3685  raltpg  4073  tpss  4187  dfopif  4205  disjxun  4440  otth2  4723  otthg  4725  oteqex  4735  poirr  4806  po3nr  4809  wefrc  4868  rabxp  5030  brinxp2  5055  brinxp  5056  f1orn  5819  dff1o6  6162  oprabid  6301  oprabv  6322  ndmovass  6440  elovmpt2  6497  elovmpt2rab  6498  elovmpt2rab1  6499  elovmpt3rab1  6513  dfwe2  6590  opiota  6835  dfxp3  6836  bropopvvv  6855  oaord  7188  oeeui  7243  oeeu  7244  nnaord  7260  swoso  7334  fiint  7788  funsnfsupp  7844  alephval3  8482  fpwwe2lem8  9006  fpwwe2lem9  9007  fpwwe2lem12  9010  ingru  9184  axgroth3  9200  ltrelxr  9639  ltxrlt  9646  wloglei  10076  sup2  10490  rexuz2  11123  ltxr  11315  elixx3g  11533  ixxun  11536  elioo4g  11576  elioopnf  11609  elioomnf  11610  elicopnf  11611  elxrge0  11620  divelunit  11653  elfz2  11670  elfzuzb  11673  uzsplit  11741  fznn0  11760  elfzmlbp  11774  elfzo2  11791  fzolb2  11794  fzouzsplit  11819  ssfzo12bi  11866  fzind2  11883  ccatsymb  12554  swrdccatin2  12664  swrdccatin12lem2  12666  swrdccatin12lem3  12667  swrdccatin12  12668  repsdf2  12702  repswsymball  12703  repswsymballbi  12704  repswswrd  12708  abs2dif  13116  sinltx  13776  divalglem8  13908  divalglem10  13910  divalgb  13912  bitsval2  13925  rplpwr  14044  pythagtriplem2  14191  pythagtrip  14208  pwsle  14738  imasvscafn  14783  mreexmrid  14889  iscatd2  14927  issect  15000  issect2  15001  oppcsect  15020  isfunc  15082  funcpropd  15118  fucsect  15190  fucinv  15191  setcsect  15265  setcinv  15266  mndcl  15728  issubm2  15784  issubg3  16009  resgrpisgrp  16012  cycsubgcl  16017  eqgval  16040  eqger  16041  isgim  16100  gaorb  16135  gaorber  16136  gastacos  16138  symg2bas  16213  galactghm  16218  gsmsymgreqlem2  16246  pmtr3ncom  16291  ispgp  16403  efgcpbllema  16563  efgcpbllemb  16564  eqgabl  16631  dprdw  16829  dprdwOLD  16835  rngpropd  17012  rngrghm  17030  isirred2  17129  rim0to0  17169  drngid2  17190  islss  17359  islmim  17486  lmhmpropd  17497  isassa  17730  mpfrcl  17953  zndvds  18350  znleval  18355  znleval2  18356  obselocv  18521  matinvgcell  18699  mat1dimscm  18739  scmatscm  18777  scmatf1  18795  mdetunilem7  18882  cpmatacl  18979  cpmatmcl  18982  mat2pmatf1  18992  mat2pmatghm  18993  mat2pmatmul  18994  mat2pmatlin  18998  mat2pmatscmxcl  19003  m2pmfzgsumcl  19011  decpmataa0  19031  monmatcollpw  19042  pmatcollpwscmatlem1  19052  pmatcollpwscmatlem2  19053  pm2mpghm  19079  pm2mpmhmlem2  19082  monmat2matmon  19087  chfacfisf  19117  chfacfisfcpmat  19118  chfacfpmmulgsum2  19128  isbasis3g  19212  leordtvallem2  19473  lmfval  19494  lmbr  19520  lmbr2  19521  lmmo  19642  dfcon2  19681  ptbasin  19808  ptbasfi  19812  txcnpi  19839  ptcnp  19853  hausdiag  19876  qtophmeo  20048  fbunfip  20100  elflim2  20195  hausflimi  20211  isfcls  20240  isfcls2  20244  istmd  20303  istgp  20306  istrg  20396  istdrg  20398  istdrg2  20410  istlm  20417  imasdsf1olem  20606  xmeterval  20665  xmeter  20666  prdsxmslem2  20762  blval2  20808  isngp  20846  isngp2  20847  isngp3  20848  isnlm  20914  cnbl0  21011  cnblcld  21012  elii1  21165  isphtpc  21224  phtpcer  21225  iscph  21347  lmmbr  21427  lmmbr2  21428  lmmbrf  21431  iscfil2  21435  iscau3  21447  iscau4  21448  iscauf  21449  caucfil  21452  isbn  21507  ishl2  21540  ovolfcl  21608  ioombl1lem4  21701  mbfmax  21786  iblpos  21929  limcrcl  22008  ig1pval3  22305  ulmdvlem3  22526  ellogdm  22743  fsumvma2  23212  chpchtsum  23217  chpub  23218  dchrelbas3  23236  axeuclidlem  23936  axeuclid  23937  nb3grapr2  24118  nb3gra2nb  24119  0wlk  24211  0trl  24212  constr2wlk  24264  3v3e3cycl1  24308  wwlknred  24387  wwlknndef  24401  isclwlk  24420  clwwlkprop  24434  clwwlknndef  24437  clwwlknwwlkncl  24464  wwlkext2clwwlk  24467  wwlksubclwwlk  24468  clwwnisshclwwn  24473  erclwwlkref  24477  erclwwlknref  24489  clwlkfoclwwlk  24509  el2wlkonotot0  24536  el2wlkonotot  24537  el2wlkonotot1  24538  2wlkonotv  24541  usg2spthonot0  24553  cusgraisrusgra  24602  rusgranumwlkl1  24611  rusgranumwlkb0  24617  rusgra0edg  24619  rusgranumwlk  24621  frgra3v  24666  1to3vfriswmgra  24671  frgraregorufrg  24737  extwwlkfablem2  24743  numclwwlkffin  24747  numclwwlkovfel2  24748  numclwwlkovf2  24749  numclwwlkovf2ex  24751  numclwwlkovgelim  24754  numclwlk1lem2fo  24760  numclwwlk2lem1  24767  numclwwlk7  24779  nvex  25168  isnv  25169  dfadj2  26468  cnvadj  26475  adjeq  26518  eleigvec  26540  eleigvec2  26541  chirredi  26977  or3di  27031  eliccelico  27244  omndmul2  27352  isorng  27440  relogbcl  27646  eulerpartlemv  27931  eulerpartlemd  27933  eulerpartlemn  27948  prob01  27980  probun  27986  pconcon  28304  rescon  28319  iscvm  28332  cvmlift2lem12  28387  cvmlift3lem5  28396  lediv2aALT  28506  dfso3  28560  br6  28751  preduz  28845  nofulllem2  29028  nofulllem5  29031  elfuns  29130  brimg  29152  brsuccf  29156  cgrxfr  29270  segcon2  29320  seglecgr12im  29325  seglecgr12  29326  segletr  29329  btwnoutside  29340  broutsideof3  29341  outsideoftr  29344  outsidele  29347  fdc  29830  isbnd3b  29873  ablo4pnp  29934  crngm4  29992  isidlc  30004  pridl  30026  ispridl2  30027  ispridlc  30059  ts3an1  30150  ts3an2  30151  ts3an3  30152  3anrabdioph  30309  issdrg2  30743  fgraphxp  30767  rfcnnnub  30946  stoweidlem35  31292  ndmaovass  31715  rexdifpr  31724  elfz2z  31757  usgra2pth0  31781  islindeps  32004  islindeps2  32034  isldepslvec2  32036  ex3  32301  dfvd3  32325  3impexpVD  32613  bnj170  32707  bnj248  32709  bnj252  32712  bnj253  32713  bnj945  32788  bnj1098  32798  bnj1224  32816  bnj150  32890  bnj153  32894  bnj545  32909  bnj557  32915  bnj571  32920  bnj594  32926  bnj864  32936  bnj865  32937  bnj849  32939  bnj964  32957  bnj986  32968  bnj996  32969  bnj1033  32981  bnj1110  32994  bnj1128  33002  bnj1174  33015  bj-imn3ani  33134  islshpsm  33654  islshpat  33691  cmtfvalN  33884  cmtvalN  33885  ishlat1  34026  ishlat2  34027  3dim0  34130  2dim  34143  islvol5  34252  lhpexle3  34685  cdleme0ex2N  34897  cdleme0nex  34963  cdlemg2cex  35264  cdlemg33b0  35374  cdlemg33b  35380  cdlemg33c  35381  cdlemg33e  35383  dib1dim  35839  diblsmopel  35845  dihopelvalcpre  35922  lcfls1c  36210
  Copyright terms: Public domain W3C validator