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

Definition df-3an 941
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 633. (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 939 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 360 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 360 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 178 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  943  3anrot  944  3ancoma  946  3anan32  951  3anor  953  3ioran  955  3simpa  957  3pm3.2i  1135  pm3.2an3  1136  3jca  1137  3anbi123i  1145  3imp  1150  3anbi123d  1257  3anim123d  1264  an6  1266  cadan  1388  19.26-3an  1594  hb3an  1725  nf3and  1730  nf3an  1740  sb3an  1962  eeeanv  2056  mopick2  2180  r19.26-3  2639  3reeanv  2670  ceqsex3v  2764  ceqsex4v  2765  ceqsex8v  2767  elin3  3268  raltpg  3588  tpss  3679  dfopif  3693  disjxun  3918  otth2  4142  oteqex  4152  poirr  4218  po3nr  4221  wefrc  4280  dfwe2  4464  rabxp  4632  brinxp2  4658  brinxp  4659  f1orn  5339  dff1o6  5643  oprabid  5734  ndmovass  5860  elovmpt2  5916  dfxp3  6031  opiota  6174  oaord  6431  oeeui  6486  oeeu  6487  nnaord  6503  swoso  6577  fiint  7018  alephval3  7621  fpwwe2lem8  8139  fpwwe2lem9  8140  fpwwe2lem12  8143  ingru  8317  axgroth3  8333  ltrelxr  8766  ltxrlt  8773  wloglei  9185  sup2  9590  rexuz2  10149  ltxr  10336  elixx3g  10547  ixxun  10550  elioo4g  10589  elioopnf  10615  elioomnf  10616  elicopnf  10617  elxrge0  10625  elfz2  10667  elfzuzb  10670  fznn0  10729  uzsplit  10733  elfzo2  10756  fzolb2  10759  fzouzsplit  10779  fzind2  10801  abs2dif  11693  sinltx  12343  divalglem8  12473  divalglem10  12475  divalgb  12477  bitsval2  12490  rplpwr  12609  pythagtriplem2  12744  pythagtrip  12761  pwsle  13265  imasvscafn  13313  iscatd2  13427  issect  13500  issect2  13501  oppcsect  13520  isfunc  13582  funcpropd  13618  fucsect  13690  fucinv  13691  setcsect  13765  setcinv  13766  mndcl  14207  issubm2  14261  issubg3  14472  cycsubgcl  14478  eqgval  14501  eqger  14502  isgim  14561  gaorb  14596  gaorber  14597  gastacos  14599  galactghm  14618  ispgp  14738  efgcpbllema  14898  efgcpbllemb  14899  eqgabl  14966  dprdw  15080  rngpropd  15207  rngrghm  15224  isirred2  15318  drngid2  15363  islss  15527  islmim  15650  lmhmpropd  15661  isassa  15888  zndvds  16335  znleval  16340  znleval2  16341  obselocv  16460  isbasis3g  16519  leordtvallem2  16773  lmfval  16794  lmbr  16820  lmbr2  16821  lmmo  16940  dfcon2  16977  ptbasin  17104  ptbasfi  17108  txcnpi  17134  ptcnp  17148  hausdiag  17171  qtophmeo  17340  fbunfip  17396  elflim2  17491  hausflimi  17507  isfcls  17536  isfcls2  17540  istmd  17589  istgp  17592  istrg  17678  istdrg  17680  istdrg2  17692  istlm  17699  imasdsf1olem  17769  xmeterval  17810  xmeter  17811  prdsxmslem2  17907  isngp  17950  isngp2  17951  isngp3  17952  isnlm  18018  cnbl0  18115  cnblcld  18116  elii1  18265  isphtpc  18324  phtpcer  18325  iscph  18438  lmmbr  18516  lmmbr2  18517  lmmbrf  18520  iscfil2  18524  iscau3  18536  iscau4  18537  iscauf  18538  caucfil  18541  isbn  18592  ishl2  18619  ovolfcl  18658  ioombl1lem4  18750  mbfmax  18836  iblpos  18979  limcrcl  19056  mpfrcl  19234  ig1pval3  19392  ulmdvlem3  19611  ellogdm  19818  fsumvma2  20285  chpchtsum  20290  chpub  20291  dchrelbas3  20309  nvex  20997  isnv  20998  dfadj2  22295  cnvadj  22302  adjeq  22345  eleigvec  22367  eleigvec2  22368  chirredi  22804  pconcon  22933  rescon  22948  iscvm  22961  cvmlift2lem12  23016  cvmlift3lem5  23025  lediv2aALT  23184  dfso3  23245  divelunit  23250  br6  23284  preduz  23368  axfelem9  23522  brsuccf  23654  axeuclidlem  23764  axeuclid  23765  cgrxfr  23852  segcon2  23902  seglecgr12im  23907  seglecgr12  23908  segletr  23911  btwnoutside  23922  broutsideof3  23923  outsideoftr  23926  outsidele  23929  eqvinopb  24130  copsexgb  24131  elo  24206  dff1o6f  24257  prismorcsetlem  25078  prismorcset  25080  prismorcsetlemc  25083  cmppar  25139  cmppar3  25140  isibcg  25357  fdc  25621  isbnd3b  25675  ablo4pnp  25736  crngm4  25794  isidlc  25806  pridl  25828  ispridl2  25829  ispridlc  25861  3anrabdioph  26028  issdrg2  26672  fgraphxp  26696  dfvd3  27053  3impexpVD  27322  bnj170  27412  bnj248  27414  bnj252  27417  bnj253  27418  bnj945  27494  bnj1098  27504  bnj1224  27523  bnj150  27597  bnj153  27601  bnj545  27616  bnj557  27622  bnj571  27627  bnj594  27633  bnj864  27643  bnj865  27644  bnj849  27646  bnj964  27664  bnj986  27675  bnj996  27676  bnj1033  27688  bnj1110  27701  bnj1128  27709  bnj1174  27722  islshpsm  27859  islshpat  27896  cmtfvalN  28089  cmtvalN  28090  ishlat1  28231  ishlat2  28232  3dim0  28335  2dim  28348  islvol5  28457  lhpexle3  28890  cdleme0ex2N  29102  cdleme0nex  29168  cdlemg2cex  29469  cdlemg33b0  29579  cdlemg33b  29585  cdlemg33c  29586  cdlemg33e  29588  dib1dim  30044  diblsmopel  30050  dihopelvalcpre  30127  lcfls1c  30415
  Copyright terms: Public domain W3C validator