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

Definition df-3an 938
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 631. (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 936 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 359 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 359 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 177 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  940  3anrot  941  3ancoma  943  3anan32  948  3anor  950  3ioran  952  3simpa  954  3pm3.2i  1132  pm3.2an3  1133  3jca  1134  3anbi123i  1142  3imp  1147  3anbi123d  1254  3anim123d  1261  an6  1263  cadan  1398  19.26-3an  1602  nf3and  1840  nf3an  1845  hb3anOLD  1849  4exdistr  1930  eeeanv  1934  eeeanvOLD  1935  sb3an  2119  mopick2  2321  r19.26-3  2800  3reeanv  2836  ceqsex3v  2954  ceqsex4v  2955  ceqsex8v  2957  elin3  3492  raltpg  3819  tpss  3924  dfopif  3941  disjxun  4170  otth2  4399  oteqex  4409  poirr  4474  po3nr  4477  wefrc  4536  dfwe2  4721  rabxp  4873  brinxp2  4898  brinxp  4899  f1orn  5643  dff1o6  5972  oprabid  6064  ndmovass  6194  elovmpt2  6250  dfxp3  6365  bropopvvv  6385  opiota  6494  oaord  6749  oeeui  6804  oeeu  6805  nnaord  6821  swoso  6895  fiint  7342  alephval3  7947  fpwwe2lem8  8468  fpwwe2lem9  8469  fpwwe2lem12  8472  ingru  8646  axgroth3  8662  ltrelxr  9095  ltxrlt  9102  wloglei  9515  sup2  9920  rexuz2  10484  ltxr  10671  elixx3g  10885  ixxun  10888  elioo4g  10927  elioopnf  10954  elioomnf  10955  elicopnf  10956  elxrge0  10964  elfz2  11006  elfzuzb  11009  fznn0  11069  uzsplit  11073  elfzo2  11098  fzolb2  11101  fzouzsplit  11123  fzind2  11153  abs2dif  12091  sinltx  12745  divalglem8  12875  divalglem10  12877  divalgb  12879  bitsval2  12892  rplpwr  13011  pythagtriplem2  13146  pythagtrip  13163  pwsle  13669  imasvscafn  13717  mreexmrid  13823  iscatd2  13861  issect  13934  issect2  13935  oppcsect  13954  isfunc  14016  funcpropd  14052  fucsect  14124  fucinv  14125  setcsect  14199  setcinv  14200  mndcl  14650  issubm2  14704  issubg3  14915  cycsubgcl  14921  eqgval  14944  eqger  14945  isgim  15004  gaorb  15039  gaorber  15040  gastacos  15042  galactghm  15061  ispgp  15181  efgcpbllema  15341  efgcpbllemb  15342  eqgabl  15409  dprdw  15523  rngpropd  15650  rngrghm  15667  isirred2  15761  drngid2  15806  islss  15966  islmim  16089  lmhmpropd  16100  isassa  16330  zndvds  16785  znleval  16790  znleval2  16791  obselocv  16910  isbasis3g  16969  leordtvallem2  17229  lmfval  17250  lmbr  17276  lmbr2  17277  lmmo  17398  dfcon2  17435  ptbasin  17562  ptbasfi  17566  txcnpi  17593  ptcnp  17607  hausdiag  17630  qtophmeo  17802  fbunfip  17854  elflim2  17949  hausflimi  17965  isfcls  17994  isfcls2  17998  istmd  18057  istgp  18060  istrg  18146  istdrg  18148  istdrg2  18160  istlm  18167  imasdsf1olem  18356  xmeterval  18415  xmeter  18416  prdsxmslem2  18512  blval2  18558  isngp  18596  isngp2  18597  isngp3  18598  isnlm  18664  cnbl0  18761  cnblcld  18762  elii1  18913  isphtpc  18972  phtpcer  18973  iscph  19086  lmmbr  19164  lmmbr2  19165  lmmbrf  19168  iscfil2  19172  iscau3  19184  iscau4  19185  iscauf  19186  caucfil  19189  isbn  19244  ishl2  19277  ovolfcl  19316  ioombl1lem4  19408  mbfmax  19494  iblpos  19637  limcrcl  19714  mpfrcl  19892  ig1pval3  20050  ulmdvlem3  20271  ellogdm  20483  fsumvma2  20951  chpchtsum  20956  chpub  20957  dchrelbas3  20975  nb3grapr2  21416  nb3gra2nb  21417  0wlk  21498  0trl  21499  constr2wlk  21551  3v3e3cycl1  21584  nvex  22043  isnv  22044  dfadj2  23341  cnvadj  23348  adjeq  23391  eleigvec  23413  eleigvec2  23414  chirredi  23850  or3di  23904  eliccelico  24093  relogbcl  24355  prob01  24624  probun  24630  pconcon  24871  rescon  24886  iscvm  24899  cvmlift2lem12  24954  cvmlift3lem5  24963  lediv2aALT  25070  dfso3  25130  divelunit  25138  br6  25328  preduz  25414  nofulllem2  25571  nofulllem5  25574  brsuccf  25694  axeuclidlem  25805  axeuclid  25806  cgrxfr  25893  segcon2  25943  seglecgr12im  25948  seglecgr12  25949  segletr  25952  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsidele  25970  fdc  26339  isbnd3b  26384  ablo4pnp  26445  crngm4  26503  isidlc  26515  pridl  26537  ispridl2  26538  ispridlc  26570  3anrabdioph  26731  issdrg2  27374  fgraphxp  27398  rfcnnnub  27574  stoweidlem35  27651  ndmaovass  27937  rexdifpr  27947  otthg  27952  elfzmlbp  27978  nn0fz0  27979  swrdccatin2  28018  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  usgra2pth0  28042  el2wlkonotot0  28069  el2wlkonotot  28070  el2wlkonotot1  28071  2wlkonotv  28074  usg2spthonot0  28086  frgra3v  28106  1to3vfriswmgra  28111  dfvd3  28392  3impexpVD  28677  bnj170  28768  bnj248  28770  bnj252  28773  bnj253  28774  bnj945  28850  bnj1098  28860  bnj1224  28879  bnj150  28953  bnj153  28957  bnj545  28972  bnj557  28978  bnj571  28983  bnj594  28989  bnj864  28999  bnj865  29000  bnj849  29002  bnj964  29020  bnj986  29031  bnj996  29032  bnj1033  29044  bnj1110  29057  bnj1128  29065  bnj1174  29078  sb3anNEW7  29341  eeeanvOLD7  29388  islshpsm  29463  islshpat  29500  cmtfvalN  29693  cmtvalN  29694  ishlat1  29835  ishlat2  29836  3dim0  29939  2dim  29952  islvol5  30061  lhpexle3  30494  cdleme0ex2N  30706  cdleme0nex  30772  cdlemg2cex  31073  cdlemg33b0  31183  cdlemg33b  31189  cdlemg33c  31190  cdlemg33e  31192  dib1dim  31648  diblsmopel  31654  dihopelvalcpre  31731  lcfls1c  32019
  Copyright terms: Public domain W3C validator