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  2127  mopick2  2329  r19.26-3  2808  3reeanv  2844  ceqsex3v  2962  ceqsex4v  2963  ceqsex8v  2965  elin3  3500  raltpg  3827  tpss  3932  dfopif  3949  disjxun  4178  otth2  4407  oteqex  4417  poirr  4482  po3nr  4485  wefrc  4544  dfwe2  4729  rabxp  4881  brinxp2  4906  brinxp  4907  f1orn  5651  dff1o6  5980  oprabid  6072  ndmovass  6202  elovmpt2  6258  dfxp3  6373  bropopvvv  6393  opiota  6502  oaord  6757  oeeui  6812  oeeu  6813  nnaord  6829  swoso  6903  fiint  7350  alephval3  7955  fpwwe2lem8  8476  fpwwe2lem9  8477  fpwwe2lem12  8480  ingru  8654  axgroth3  8670  ltrelxr  9103  ltxrlt  9110  wloglei  9523  sup2  9928  rexuz2  10492  ltxr  10679  elixx3g  10893  ixxun  10896  elioo4g  10935  elioopnf  10962  elioomnf  10963  elicopnf  10964  elxrge0  10972  elfz2  11014  elfzuzb  11017  fznn0  11077  uzsplit  11081  elfzo2  11106  fzolb2  11109  fzouzsplit  11131  fzind2  11161  abs2dif  12099  sinltx  12753  divalglem8  12883  divalglem10  12885  divalgb  12887  bitsval2  12900  rplpwr  13019  pythagtriplem2  13154  pythagtrip  13171  pwsle  13677  imasvscafn  13725  mreexmrid  13831  iscatd2  13869  issect  13942  issect2  13943  oppcsect  13962  isfunc  14024  funcpropd  14060  fucsect  14132  fucinv  14133  setcsect  14207  setcinv  14208  mndcl  14658  issubm2  14712  issubg3  14923  cycsubgcl  14929  eqgval  14952  eqger  14953  isgim  15012  gaorb  15047  gaorber  15048  gastacos  15050  galactghm  15069  ispgp  15189  efgcpbllema  15349  efgcpbllemb  15350  eqgabl  15417  dprdw  15531  rngpropd  15658  rngrghm  15675  isirred2  15769  drngid2  15814  islss  15974  islmim  16097  lmhmpropd  16108  isassa  16338  zndvds  16793  znleval  16798  znleval2  16799  obselocv  16918  isbasis3g  16977  leordtvallem2  17237  lmfval  17258  lmbr  17284  lmbr2  17285  lmmo  17406  dfcon2  17443  ptbasin  17570  ptbasfi  17574  txcnpi  17601  ptcnp  17615  hausdiag  17638  qtophmeo  17810  fbunfip  17862  elflim2  17957  hausflimi  17973  isfcls  18002  isfcls2  18006  istmd  18065  istgp  18068  istrg  18154  istdrg  18156  istdrg2  18168  istlm  18175  imasdsf1olem  18364  xmeterval  18423  xmeter  18424  prdsxmslem2  18520  blval2  18566  isngp  18604  isngp2  18605  isngp3  18606  isnlm  18672  cnbl0  18769  cnblcld  18770  elii1  18921  isphtpc  18980  phtpcer  18981  iscph  19094  lmmbr  19172  lmmbr2  19173  lmmbrf  19176  iscfil2  19180  iscau3  19192  iscau4  19193  iscauf  19194  caucfil  19197  isbn  19252  ishl2  19285  ovolfcl  19324  ioombl1lem4  19416  mbfmax  19502  iblpos  19645  limcrcl  19722  mpfrcl  19900  ig1pval3  20058  ulmdvlem3  20279  ellogdm  20491  fsumvma2  20959  chpchtsum  20964  chpub  20965  dchrelbas3  20983  nb3grapr2  21424  nb3gra2nb  21425  0wlk  21506  0trl  21507  constr2wlk  21559  3v3e3cycl1  21592  nvex  22051  isnv  22052  dfadj2  23349  cnvadj  23356  adjeq  23399  eleigvec  23421  eleigvec2  23422  chirredi  23858  or3di  23912  eliccelico  24101  relogbcl  24363  prob01  24632  probun  24638  pconcon  24879  rescon  24894  iscvm  24907  cvmlift2lem12  24962  cvmlift3lem5  24971  lediv2aALT  25078  dfso3  25138  divelunit  25146  br6  25336  preduz  25422  nofulllem2  25579  nofulllem5  25582  brsuccf  25702  axeuclidlem  25813  axeuclid  25814  cgrxfr  25901  segcon2  25951  seglecgr12im  25956  seglecgr12  25957  segletr  25960  btwnoutside  25971  broutsideof3  25972  outsideoftr  25975  outsidele  25978  fdc  26347  isbnd3b  26392  ablo4pnp  26453  crngm4  26511  isidlc  26523  pridl  26545  ispridl2  26546  ispridlc  26578  3anrabdioph  26739  issdrg2  27382  fgraphxp  27406  rfcnnnub  27582  stoweidlem35  27659  ndmaovass  27945  rexdifpr  27955  otthg  27960  elfzmlbp  27986  nn0fz0  27987  swrdccatin2  28026  swrdccatin12lem3  28032  swrdccatin12lem4  28033  swrdccatin12  28034  usgra2pth0  28050  el2wlkonotot0  28077  el2wlkonotot  28078  el2wlkonotot1  28079  2wlkonotv  28082  usg2spthonot0  28094  frgra3v  28114  1to3vfriswmgra  28119  ex3  28377  dfvd3  28401  3impexpVD  28686  bnj170  28780  bnj248  28782  bnj252  28785  bnj253  28786  bnj945  28862  bnj1098  28872  bnj1224  28891  bnj150  28965  bnj153  28969  bnj545  28984  bnj557  28990  bnj571  28995  bnj594  29001  bnj864  29011  bnj865  29012  bnj849  29014  bnj964  29032  bnj986  29043  bnj996  29044  bnj1033  29056  bnj1110  29069  bnj1128  29077  bnj1174  29090  sb3anNEW7  29353  eeeanvOLD7  29400  islshpsm  29475  islshpat  29512  cmtfvalN  29705  cmtvalN  29706  ishlat1  29847  ishlat2  29848  3dim0  29951  2dim  29964  islvol5  30073  lhpexle3  30506  cdleme0ex2N  30718  cdleme0nex  30784  cdlemg2cex  31085  cdlemg33b0  31195  cdlemg33b  31201  cdlemg33c  31202  cdlemg33e  31204  dib1dim  31660  diblsmopel  31666  dihopelvalcpre  31743  lcfls1c  32031
  Copyright terms: Public domain W3C validator