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 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 632. (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 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  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  1384  19.26-3an  1583  hb3an  1760  nf3and  1765  nf3an  1775  eeeanv  1856  sb3an  2009  mopick2  2211  r19.26-3  2678  3reeanv  2709  ceqsex3v  2827  ceqsex4v  2828  ceqsex8v  2830  elin3  3361  raltpg  3685  tpss  3780  dfopif  3794  disjxun  4022  otth2  4248  oteqex  4258  poirr  4324  po3nr  4327  wefrc  4386  dfwe2  4572  rabxp  4724  brinxp2  4750  brinxp  4751  f1orn  5447  dff1o6  5752  oprabid  5843  ndmovass  5969  elovmpt2  6025  dfxp3  6140  opiota  6283  oaord  6540  oeeui  6595  oeeu  6596  nnaord  6612  swoso  6686  fiint  7128  alephval3  7732  fpwwe2lem8  8254  fpwwe2lem9  8255  fpwwe2lem12  8258  ingru  8432  axgroth3  8448  ltrelxr  8881  ltxrlt  8888  wloglei  9300  sup2  9705  rexuz2  10265  ltxr  10452  elixx3g  10663  ixxun  10666  elioo4g  10705  elioopnf  10731  elioomnf  10732  elicopnf  10733  elxrge0  10741  elfz2  10783  elfzuzb  10786  fznn0  10845  uzsplit  10849  elfzo2  10872  fzolb2  10875  fzouzsplit  10895  fzind2  10917  abs2dif  11810  sinltx  12463  divalglem8  12593  divalglem10  12595  divalgb  12597  bitsval2  12610  rplpwr  12729  pythagtriplem2  12864  pythagtrip  12881  pwsle  13385  imasvscafn  13433  mreexmrid  13539  iscatd2  13577  issect  13650  issect2  13651  oppcsect  13670  isfunc  13732  funcpropd  13768  fucsect  13840  fucinv  13841  setcsect  13915  setcinv  13916  mndcl  14366  issubm2  14420  issubg3  14631  cycsubgcl  14637  eqgval  14660  eqger  14661  isgim  14720  gaorb  14755  gaorber  14756  gastacos  14758  galactghm  14777  ispgp  14897  efgcpbllema  15057  efgcpbllemb  15058  eqgabl  15125  dprdw  15239  rngpropd  15366  rngrghm  15383  isirred2  15477  drngid2  15522  islss  15686  islmim  15809  lmhmpropd  15820  isassa  16050  zndvds  16497  znleval  16502  znleval2  16503  obselocv  16622  isbasis3g  16681  leordtvallem2  16935  lmfval  16956  lmbr  16982  lmbr2  16983  lmmo  17102  dfcon2  17139  ptbasin  17266  ptbasfi  17270  txcnpi  17296  ptcnp  17310  hausdiag  17333  qtophmeo  17502  fbunfip  17558  elflim2  17653  hausflimi  17669  isfcls  17698  isfcls2  17702  istmd  17751  istgp  17754  istrg  17840  istdrg  17842  istdrg2  17854  istlm  17861  imasdsf1olem  17931  xmeterval  17972  xmeter  17973  prdsxmslem2  18069  isngp  18112  isngp2  18113  isngp3  18114  isnlm  18180  cnbl0  18277  cnblcld  18278  elii1  18427  isphtpc  18486  phtpcer  18487  iscph  18600  lmmbr  18678  lmmbr2  18679  lmmbrf  18682  iscfil2  18686  iscau3  18698  iscau4  18699  iscauf  18700  caucfil  18703  isbn  18754  ishl2  18781  ovolfcl  18820  ioombl1lem4  18912  mbfmax  18998  iblpos  19141  limcrcl  19218  mpfrcl  19396  ig1pval3  19554  ulmdvlem3  19773  ellogdm  19980  fsumvma2  20447  chpchtsum  20452  chpub  20453  dchrelbas3  20471  nvex  21159  isnv  21160  dfadj2  22457  cnvadj  22464  adjeq  22507  eleigvec  22529  eleigvec2  22530  chirredi  22966  ballotlem2  23040  pconcon  23166  rescon  23181  iscvm  23194  cvmlift2lem12  23249  cvmlift3lem5  23258  lediv2aALT  23417  dfso3  23478  divelunit  23483  br6  23517  preduz  23601  axfelem9  23755  brsuccf  23887  axeuclidlem  23997  axeuclid  23998  cgrxfr  24085  segcon2  24135  seglecgr12im  24140  seglecgr12  24141  segletr  24144  btwnoutside  24155  broutsideof3  24156  outsideoftr  24159  outsidele  24162  eqvinopb  24363  copsexgb  24364  elo  24439  dff1o6f  24490  prismorcsetlem  25311  prismorcset  25313  prismorcsetlemc  25316  cmppar  25372  cmppar3  25373  isibcg  25590  fdc  25854  isbnd3b  25908  ablo4pnp  25969  crngm4  26027  isidlc  26039  pridl  26061  ispridl2  26062  ispridlc  26094  3anrabdioph  26261  issdrg2  26905  fgraphxp  26929  rfcnnnub  27106  stoweidlem35  27183  ndmaovass  27445  dfvd3  27631  3impexpVD  27900  bnj170  27990  bnj248  27992  bnj252  27995  bnj253  27996  bnj945  28072  bnj1098  28082  bnj1224  28101  bnj150  28175  bnj153  28179  bnj545  28194  bnj557  28200  bnj571  28205  bnj594  28211  bnj864  28221  bnj865  28222  bnj849  28224  bnj964  28242  bnj986  28253  bnj996  28254  bnj1033  28266  bnj1110  28279  bnj1128  28287  bnj1174  28300  islshpsm  28437  islshpat  28474  cmtfvalN  28667  cmtvalN  28668  ishlat1  28809  ishlat2  28810  3dim0  28913  2dim  28926  islvol5  29035  lhpexle3  29468  cdleme0ex2N  29680  cdleme0nex  29746  cdlemg2cex  30047  cdlemg33b0  30157  cdlemg33b  30163  cdlemg33c  30164  cdlemg33e  30166  dib1dim  30622  diblsmopel  30628  dihopelvalcpre  30705  lcfls1c  30993
  Copyright terms: Public domain W3C validator