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  1401  19.26-3an  1605  nf3and  1844  nf3an  1849  hb3anOLD  1853  4exdistr  1934  eeeanv  1938  eeeanvOLD  1939  sb3an  2144  mopick2  2347  r19.26-3  2832  3reeanv  2868  ceqsex3v  2986  ceqsex4v  2987  ceqsex8v  2989  elin3  3524  raltpg  3851  tpss  3956  dfopif  3973  disjxun  4202  otth2  4431  oteqex  4441  poirr  4506  po3nr  4509  wefrc  4568  dfwe2  4753  rabxp  4905  brinxp2  4930  brinxp  4931  f1orn  5675  dff1o6  6004  oprabid  6096  ndmovass  6226  elovmpt2  6282  dfxp3  6397  bropopvvv  6417  opiota  6526  oaord  6781  oeeui  6836  oeeu  6837  nnaord  6853  swoso  6927  fiint  7374  alephval3  7980  fpwwe2lem8  8501  fpwwe2lem9  8502  fpwwe2lem12  8505  ingru  8679  axgroth3  8695  ltrelxr  9128  ltxrlt  9135  wloglei  9548  sup2  9953  rexuz2  10517  ltxr  10704  elixx3g  10918  ixxun  10921  elioo4g  10960  elioopnf  10987  elioomnf  10988  elicopnf  10989  elxrge0  10997  elfz2  11039  elfzuzb  11042  fznn0  11102  uzsplit  11106  elfzo2  11131  fzolb2  11134  fzouzsplit  11156  fzind2  11186  abs2dif  12124  sinltx  12778  divalglem8  12908  divalglem10  12910  divalgb  12912  bitsval2  12925  rplpwr  13044  pythagtriplem2  13179  pythagtrip  13196  pwsle  13702  imasvscafn  13750  mreexmrid  13856  iscatd2  13894  issect  13967  issect2  13968  oppcsect  13987  isfunc  14049  funcpropd  14085  fucsect  14157  fucinv  14158  setcsect  14232  setcinv  14233  mndcl  14683  issubm2  14737  issubg3  14948  cycsubgcl  14954  eqgval  14977  eqger  14978  isgim  15037  gaorb  15072  gaorber  15073  gastacos  15075  galactghm  15094  ispgp  15214  efgcpbllema  15374  efgcpbllemb  15375  eqgabl  15442  dprdw  15556  rngpropd  15683  rngrghm  15700  isirred2  15794  drngid2  15839  islss  15999  islmim  16122  lmhmpropd  16133  isassa  16363  zndvds  16818  znleval  16823  znleval2  16824  obselocv  16943  isbasis3g  17002  leordtvallem2  17263  lmfval  17284  lmbr  17310  lmbr2  17311  lmmo  17432  dfcon2  17470  ptbasin  17597  ptbasfi  17601  txcnpi  17628  ptcnp  17642  hausdiag  17665  qtophmeo  17837  fbunfip  17889  elflim2  17984  hausflimi  18000  isfcls  18029  isfcls2  18033  istmd  18092  istgp  18095  istrg  18181  istdrg  18183  istdrg2  18195  istlm  18202  imasdsf1olem  18391  xmeterval  18450  xmeter  18451  prdsxmslem2  18547  blval2  18593  isngp  18631  isngp2  18632  isngp3  18633  isnlm  18699  cnbl0  18796  cnblcld  18797  elii1  18948  isphtpc  19007  phtpcer  19008  iscph  19121  lmmbr  19199  lmmbr2  19200  lmmbrf  19203  iscfil2  19207  iscau3  19219  iscau4  19220  iscauf  19221  caucfil  19224  isbn  19279  ishl2  19312  ovolfcl  19351  ioombl1lem4  19443  mbfmax  19529  iblpos  19672  limcrcl  19749  mpfrcl  19927  ig1pval3  20085  ulmdvlem3  20306  ellogdm  20518  fsumvma2  20986  chpchtsum  20991  chpub  20992  dchrelbas3  21010  nb3grapr2  21451  nb3gra2nb  21452  0wlk  21533  0trl  21534  constr2wlk  21586  3v3e3cycl1  21619  nvex  22078  isnv  22079  dfadj2  23376  cnvadj  23383  adjeq  23426  eleigvec  23448  eleigvec2  23449  chirredi  23885  or3di  23939  eliccelico  24128  relogbcl  24390  prob01  24659  probun  24665  pconcon  24906  rescon  24921  iscvm  24934  cvmlift2lem12  24989  cvmlift3lem5  24998  lediv2aALT  25105  dfso3  25165  divelunit  25173  br6  25369  preduz  25455  nofulllem2  25612  nofulllem5  25615  brimg  25732  brsuccf  25736  axeuclidlem  25849  axeuclid  25850  cgrxfr  25937  segcon2  25987  seglecgr12im  25992  seglecgr12  25993  segletr  25996  btwnoutside  26007  broutsideof3  26008  outsideoftr  26011  outsidele  26014  fdc  26386  isbnd3b  26431  ablo4pnp  26492  crngm4  26550  isidlc  26562  pridl  26584  ispridl2  26585  ispridlc  26617  3anrabdioph  26778  issdrg2  27421  fgraphxp  27445  rfcnnnub  27621  stoweidlem35  27698  ndmaovass  27984  rexdifpr  27995  otthg  28000  elfzmlbp  28028  nn0fz0  28029  swrdccatin2  28093  swrdccatin12lem3  28099  swrdccatin12lem4  28100  swrdccatin12  28101  shwrdeqdif2s  28157  usgra2pth0  28186  el2wlkonotot0  28213  el2wlkonotot  28214  el2wlkonotot1  28215  2wlkonotv  28218  usg2spthonot0  28230  frgra3v  28250  1to3vfriswmgra  28255  ex3  28513  dfvd3  28537  3impexpVD  28822  bnj170  28916  bnj248  28918  bnj252  28921  bnj253  28922  bnj945  28998  bnj1098  29008  bnj1224  29027  bnj150  29101  bnj153  29105  bnj545  29120  bnj557  29126  bnj571  29131  bnj594  29137  bnj864  29147  bnj865  29148  bnj849  29150  bnj964  29168  bnj986  29179  bnj996  29180  bnj1033  29192  bnj1110  29205  bnj1128  29213  bnj1174  29226  sb3anNEW7  29489  eeeanvOLD7  29543  islshpsm  29617  islshpat  29654  cmtfvalN  29847  cmtvalN  29848  ishlat1  29989  ishlat2  29990  3dim0  30093  2dim  30106  islvol5  30215  lhpexle3  30648  cdleme0ex2N  30860  cdleme0nex  30926  cdlemg2cex  31227  cdlemg33b0  31337  cdlemg33b  31343  cdlemg33c  31344  cdlemg33e  31346  dib1dim  31802  diblsmopel  31808  dihopelvalcpre  31885  lcfls1c  32173
  Copyright terms: Public domain W3C validator