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

Definition df-3an 936
Description: Define conjunction ('and') of 3 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 630. (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 934 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 358 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 358 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 176 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  938  3anrot  939  3ancoma  941  3anan32  946  3anor  948  3ioran  950  3simpa  952  3pm3.2i  1130  pm3.2an3  1131  3jca  1132  3anbi123i  1140  3imp  1145  3anbi123d  1252  3anim123d  1259  an6  1261  cadan  1382  19.26-3an  1582  hb3an  1759  nf3and  1764  nf3an  1774  eeeanv  1855  sb3an  2010  mopick2  2210  r19.26-3  2677  3reeanv  2708  ceqsex3v  2826  ceqsex4v  2827  ceqsex8v  2829  elin3  3360  raltpg  3684  tpss  3779  dfopif  3793  disjxun  4021  otth2  4249  oteqex  4259  poirr  4325  po3nr  4328  wefrc  4387  dfwe2  4573  rabxp  4725  brinxp2  4751  brinxp  4752  f1orn  5482  dff1o6  5791  oprabid  5882  ndmovass  6008  elovmpt2  6064  dfxp3  6179  opiota  6290  oaord  6545  oeeui  6600  oeeu  6601  nnaord  6617  swoso  6691  fiint  7133  alephval3  7737  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  ingru  8437  axgroth3  8453  ltrelxr  8886  ltxrlt  8893  wloglei  9305  sup2  9710  rexuz2  10270  ltxr  10457  elixx3g  10669  ixxun  10672  elioo4g  10711  elioopnf  10737  elioomnf  10738  elicopnf  10739  elxrge0  10747  elfz2  10789  elfzuzb  10792  fznn0  10851  uzsplit  10855  elfzo2  10878  fzolb2  10881  fzouzsplit  10901  fzind2  10923  abs2dif  11816  sinltx  12469  divalglem8  12599  divalglem10  12601  divalgb  12603  bitsval2  12616  rplpwr  12735  pythagtriplem2  12870  pythagtrip  12887  pwsle  13391  imasvscafn  13439  mreexmrid  13545  iscatd2  13583  issect  13656  issect2  13657  oppcsect  13676  isfunc  13738  funcpropd  13774  fucsect  13846  fucinv  13847  setcsect  13921  setcinv  13922  mndcl  14372  issubm2  14426  issubg3  14637  cycsubgcl  14643  eqgval  14666  eqger  14667  isgim  14726  gaorb  14761  gaorber  14762  gastacos  14764  galactghm  14783  ispgp  14903  efgcpbllema  15063  efgcpbllemb  15064  eqgabl  15131  dprdw  15245  rngpropd  15372  rngrghm  15389  isirred2  15483  drngid2  15528  islss  15692  islmim  15815  lmhmpropd  15826  isassa  16056  zndvds  16503  znleval  16508  znleval2  16509  obselocv  16628  isbasis3g  16687  leordtvallem2  16941  lmfval  16962  lmbr  16988  lmbr2  16989  lmmo  17108  dfcon2  17145  ptbasin  17272  ptbasfi  17276  txcnpi  17302  ptcnp  17316  hausdiag  17339  qtophmeo  17508  fbunfip  17564  elflim2  17659  hausflimi  17675  isfcls  17704  isfcls2  17708  istmd  17757  istgp  17760  istrg  17846  istdrg  17848  istdrg2  17860  istlm  17867  imasdsf1olem  17937  xmeterval  17978  xmeter  17979  prdsxmslem2  18075  isngp  18118  isngp2  18119  isngp3  18120  isnlm  18186  cnbl0  18283  cnblcld  18284  elii1  18433  isphtpc  18492  phtpcer  18493  iscph  18606  lmmbr  18684  lmmbr2  18685  lmmbrf  18688  iscfil2  18692  iscau3  18704  iscau4  18705  iscauf  18706  caucfil  18709  isbn  18760  ishl2  18787  ovolfcl  18826  ioombl1lem4  18918  mbfmax  19004  iblpos  19147  limcrcl  19224  mpfrcl  19402  ig1pval3  19560  ulmdvlem3  19779  ellogdm  19986  fsumvma2  20453  chpchtsum  20458  chpub  20459  dchrelbas3  20477  nvex  21167  isnv  21168  dfadj2  22465  cnvadj  22472  adjeq  22515  eleigvec  22537  eleigvec2  22538  chirredi  22974  ballotlem2  23047  or3di  23123  eliccelico  23270  relogbcl  23404  prob01  23616  probun  23622  pconcon  23762  rescon  23777  iscvm  23790  cvmlift2lem12  23845  cvmlift3lem5  23854  lediv2aALT  24013  dfso3  24074  divelunit  24080  br6  24114  preduz  24200  nofulllem2  24357  nofulllem5  24360  brsuccf  24480  axeuclidlem  24590  axeuclid  24591  cgrxfr  24678  segcon2  24728  seglecgr12im  24733  seglecgr12  24734  segletr  24737  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsidele  24755  eqvinopb  24965  copsexgb  24966  elo  25041  dff1o6f  25092  prismorcsetlem  25912  prismorcset  25914  prismorcsetlemc  25917  cmppar  25973  cmppar3  25974  isibcg  26191  fdc  26455  isbnd3b  26509  ablo4pnp  26570  crngm4  26628  isidlc  26640  pridl  26662  ispridl2  26663  ispridlc  26695  3anrabdioph  26862  issdrg2  27506  fgraphxp  27530  rfcnnnub  27707  stoweidlem35  27784  ndmaovass  28066  frgra3v  28180  1to3vfriswmgra  28185  dfvd3  28360  3impexpVD  28632  bnj170  28723  bnj248  28725  bnj252  28728  bnj253  28729  bnj945  28805  bnj1098  28815  bnj1224  28834  bnj150  28908  bnj153  28912  bnj545  28927  bnj557  28933  bnj571  28938  bnj594  28944  bnj864  28954  bnj865  28955  bnj849  28957  bnj964  28975  bnj986  28986  bnj996  28987  bnj1033  28999  bnj1110  29012  bnj1128  29020  bnj1174  29033  islshpsm  29170  islshpat  29207  cmtfvalN  29400  cmtvalN  29401  ishlat1  29542  ishlat2  29543  3dim0  29646  2dim  29659  islvol5  29768  lhpexle3  30201  cdleme0ex2N  30413  cdleme0nex  30479  cdlemg2cex  30780  cdlemg33b0  30890  cdlemg33b  30896  cdlemg33c  30897  cdlemg33e  30899  dib1dim  31355  diblsmopel  31361  dihopelvalcpre  31438  lcfls1c  31726
  Copyright terms: Public domain W3C validator