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  1963  eeeanv  2059  mopick2  2183  r19.26-3  2648  3reeanv  2679  ceqsex3v  2777  ceqsex4v  2778  ceqsex8v  2780  elin3  3302  raltpg  3625  tpss  3720  dfopif  3734  disjxun  3961  otth2  4186  oteqex  4196  poirr  4262  po3nr  4265  wefrc  4324  dfwe2  4510  rabxp  4678  brinxp2  4704  brinxp  4705  f1orn  5385  dff1o6  5690  oprabid  5781  ndmovass  5907  elovmpt2  5963  dfxp3  6078  opiota  6221  oaord  6478  oeeui  6533  oeeu  6534  nnaord  6550  swoso  6624  fiint  7066  alephval3  7670  fpwwe2lem8  8192  fpwwe2lem9  8193  fpwwe2lem12  8196  ingru  8370  axgroth3  8386  ltrelxr  8819  ltxrlt  8826  wloglei  9238  sup2  9643  rexuz2  10202  ltxr  10389  elixx3g  10600  ixxun  10603  elioo4g  10642  elioopnf  10668  elioomnf  10669  elicopnf  10670  elxrge0  10678  elfz2  10720  elfzuzb  10723  fznn0  10782  uzsplit  10786  elfzo2  10809  fzolb2  10812  fzouzsplit  10832  fzind2  10854  abs2dif  11746  sinltx  12396  divalglem8  12526  divalglem10  12528  divalgb  12530  bitsval2  12543  rplpwr  12662  pythagtriplem2  12797  pythagtrip  12814  pwsle  13318  imasvscafn  13366  mreexmrid  13472  iscatd2  13510  issect  13583  issect2  13584  oppcsect  13603  isfunc  13665  funcpropd  13701  fucsect  13773  fucinv  13774  setcsect  13848  setcinv  13849  mndcl  14299  issubm2  14353  issubg3  14564  cycsubgcl  14570  eqgval  14593  eqger  14594  isgim  14653  gaorb  14688  gaorber  14689  gastacos  14691  galactghm  14710  ispgp  14830  efgcpbllema  14990  efgcpbllemb  14991  eqgabl  15058  dprdw  15172  rngpropd  15299  rngrghm  15316  isirred2  15410  drngid2  15455  islss  15619  islmim  15742  lmhmpropd  15753  isassa  15983  zndvds  16430  znleval  16435  znleval2  16436  obselocv  16555  isbasis3g  16614  leordtvallem2  16868  lmfval  16889  lmbr  16915  lmbr2  16916  lmmo  17035  dfcon2  17072  ptbasin  17199  ptbasfi  17203  txcnpi  17229  ptcnp  17243  hausdiag  17266  qtophmeo  17435  fbunfip  17491  elflim2  17586  hausflimi  17602  isfcls  17631  isfcls2  17635  istmd  17684  istgp  17687  istrg  17773  istdrg  17775  istdrg2  17787  istlm  17794  imasdsf1olem  17864  xmeterval  17905  xmeter  17906  prdsxmslem2  18002  isngp  18045  isngp2  18046  isngp3  18047  isnlm  18113  cnbl0  18210  cnblcld  18211  elii1  18360  isphtpc  18419  phtpcer  18420  iscph  18533  lmmbr  18611  lmmbr2  18612  lmmbrf  18615  iscfil2  18619  iscau3  18631  iscau4  18632  iscauf  18633  caucfil  18636  isbn  18687  ishl2  18714  ovolfcl  18753  ioombl1lem4  18845  mbfmax  18931  iblpos  19074  limcrcl  19151  mpfrcl  19329  ig1pval3  19487  ulmdvlem3  19706  ellogdm  19913  fsumvma2  20380  chpchtsum  20385  chpub  20386  dchrelbas3  20404  nvex  21092  isnv  21093  dfadj2  22390  cnvadj  22397  adjeq  22440  eleigvec  22462  eleigvec2  22463  chirredi  22899  ballotlem2  22973  pconcon  23099  rescon  23114  iscvm  23127  cvmlift2lem12  23182  cvmlift3lem5  23191  lediv2aALT  23350  dfso3  23411  divelunit  23416  br6  23450  preduz  23534  axfelem9  23688  brsuccf  23820  axeuclidlem  23930  axeuclid  23931  cgrxfr  24018  segcon2  24068  seglecgr12im  24073  seglecgr12  24074  segletr  24077  btwnoutside  24088  broutsideof3  24089  outsideoftr  24092  outsidele  24095  eqvinopb  24296  copsexgb  24297  elo  24372  dff1o6f  24423  prismorcsetlem  25244  prismorcset  25246  prismorcsetlemc  25249  cmppar  25305  cmppar3  25306  isibcg  25523  fdc  25787  isbnd3b  25841  ablo4pnp  25902  crngm4  25960  isidlc  25972  pridl  25994  ispridl2  25995  ispridlc  26027  3anrabdioph  26194  issdrg2  26838  fgraphxp  26862  rfcnnnub  27040  stoweidlem35  27084  dfvd3  27376  3impexpVD  27645  bnj170  27735  bnj248  27737  bnj252  27740  bnj253  27741  bnj945  27817  bnj1098  27827  bnj1224  27846  bnj150  27920  bnj153  27924  bnj545  27939  bnj557  27945  bnj571  27950  bnj594  27956  bnj864  27966  bnj865  27967  bnj849  27969  bnj964  27987  bnj986  27998  bnj996  27999  bnj1033  28011  bnj1110  28024  bnj1128  28032  bnj1174  28045  islshpsm  28300  islshpat  28337  cmtfvalN  28530  cmtvalN  28531  ishlat1  28672  ishlat2  28673  3dim0  28776  2dim  28789  islvol5  28898  lhpexle3  29331  cdleme0ex2N  29543  cdleme0nex  29609  cdlemg2cex  29910  cdlemg33b0  30020  cdlemg33b  30026  cdlemg33c  30027  cdlemg33e  30029  dib1dim  30485  diblsmopel  30491  dihopelvalcpre  30568  lcfls1c  30856
  Copyright terms: Public domain W3C validator