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  pconcon  23173  rescon  23188  iscvm  23201  cvmlift2lem12  23256  cvmlift3lem5  23265  lediv2aALT  23424  dfso3  23485  divelunit  23491  br6  23525  preduz  23611  nofulllem2  23768  nofulllem5  23771  brsuccf  23891  axeuclidlem  24001  axeuclid  24002  cgrxfr  24089  segcon2  24139  seglecgr12im  24144  seglecgr12  24145  segletr  24148  btwnoutside  24159  broutsideof3  24160  outsideoftr  24163  outsidele  24166  eqvinopb  24377  copsexgb  24378  elo  24453  dff1o6f  24504  prismorcsetlem  25324  prismorcset  25326  prismorcsetlemc  25329  cmppar  25385  cmppar3  25386  isibcg  25603  fdc  25867  isbnd3b  25921  ablo4pnp  25982  crngm4  26040  isidlc  26052  pridl  26074  ispridl2  26075  ispridlc  26107  3anrabdioph  26274  issdrg2  26918  fgraphxp  26942  rfcnnnub  27119  stoweidlem35  27196  ndmaovass  27478  frgra3v  27542  1to3vfriswmgra  27547  dfvd3  27733  3impexpVD  28005  bnj170  28096  bnj248  28098  bnj252  28101  bnj253  28102  bnj945  28178  bnj1098  28188  bnj1224  28207  bnj150  28281  bnj153  28285  bnj545  28300  bnj557  28306  bnj571  28311  bnj594  28317  bnj864  28327  bnj865  28328  bnj849  28330  bnj964  28348  bnj986  28359  bnj996  28360  bnj1033  28372  bnj1110  28385  bnj1128  28393  bnj1174  28406  islshpsm  28543  islshpat  28580  cmtfvalN  28773  cmtvalN  28774  ishlat1  28915  ishlat2  28916  3dim0  29019  2dim  29032  islvol5  29141  lhpexle3  29574  cdleme0ex2N  29786  cdleme0nex  29852  cdlemg2cex  30153  cdlemg33b0  30263  cdlemg33b  30269  cdlemg33c  30270  cdlemg33e  30272  dib1dim  30728  diblsmopel  30734  dihopelvalcpre  30811  lcfls1c  31099
  Copyright terms: Public domain W3C validator