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 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 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  1585  hb3an  1771  nf3and  1776  nf3an  1786  eeeanv  1867  sb3an  2023  mopick2  2223  r19.26-3  2690  3reeanv  2721  ceqsex3v  2839  ceqsex4v  2840  ceqsex8v  2842  elin3  3373  raltpg  3697  tpss  3795  dfopif  3809  disjxun  4037  otth2  4265  oteqex  4275  poirr  4341  po3nr  4344  wefrc  4403  dfwe2  4589  rabxp  4741  brinxp2  4767  brinxp  4768  f1orn  5498  dff1o6  5807  oprabid  5898  ndmovass  6024  elovmpt2  6080  dfxp3  6195  opiota  6306  oaord  6561  oeeui  6616  oeeu  6617  nnaord  6633  swoso  6707  fiint  7149  alephval3  7753  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  ingru  8453  axgroth3  8469  ltrelxr  8902  ltxrlt  8909  wloglei  9321  sup2  9726  rexuz2  10286  ltxr  10473  elixx3g  10685  ixxun  10688  elioo4g  10727  elioopnf  10753  elioomnf  10754  elicopnf  10755  elxrge0  10763  elfz2  10805  elfzuzb  10808  fznn0  10867  uzsplit  10871  elfzo2  10894  fzolb2  10897  fzouzsplit  10917  fzind2  10939  abs2dif  11832  sinltx  12485  divalglem8  12615  divalglem10  12617  divalgb  12619  bitsval2  12632  rplpwr  12751  pythagtriplem2  12886  pythagtrip  12903  pwsle  13407  imasvscafn  13455  mreexmrid  13561  iscatd2  13599  issect  13672  issect2  13673  oppcsect  13692  isfunc  13754  funcpropd  13790  fucsect  13862  fucinv  13863  setcsect  13937  setcinv  13938  mndcl  14388  issubm2  14442  issubg3  14653  cycsubgcl  14659  eqgval  14682  eqger  14683  isgim  14742  gaorb  14777  gaorber  14778  gastacos  14780  galactghm  14799  ispgp  14919  efgcpbllema  15079  efgcpbllemb  15080  eqgabl  15147  dprdw  15261  rngpropd  15388  rngrghm  15405  isirred2  15499  drngid2  15544  islss  15708  islmim  15831  lmhmpropd  15842  isassa  16072  zndvds  16519  znleval  16524  znleval2  16525  obselocv  16644  isbasis3g  16703  leordtvallem2  16957  lmfval  16978  lmbr  17004  lmbr2  17005  lmmo  17124  dfcon2  17161  ptbasin  17288  ptbasfi  17292  txcnpi  17318  ptcnp  17332  hausdiag  17355  qtophmeo  17524  fbunfip  17580  elflim2  17675  hausflimi  17691  isfcls  17720  isfcls2  17724  istmd  17773  istgp  17776  istrg  17862  istdrg  17864  istdrg2  17876  istlm  17883  imasdsf1olem  17953  xmeterval  17994  xmeter  17995  prdsxmslem2  18091  isngp  18134  isngp2  18135  isngp3  18136  isnlm  18202  cnbl0  18299  cnblcld  18300  elii1  18449  isphtpc  18508  phtpcer  18509  iscph  18622  lmmbr  18700  lmmbr2  18701  lmmbrf  18704  iscfil2  18708  iscau3  18720  iscau4  18721  iscauf  18722  caucfil  18725  isbn  18776  ishl2  18803  ovolfcl  18842  ioombl1lem4  18934  mbfmax  19020  iblpos  19163  limcrcl  19240  mpfrcl  19418  ig1pval3  19576  ulmdvlem3  19795  ellogdm  20002  fsumvma2  20469  chpchtsum  20474  chpub  20475  dchrelbas3  20493  nvex  21183  isnv  21184  dfadj2  22481  cnvadj  22488  adjeq  22531  eleigvec  22553  eleigvec2  22554  chirredi  22990  ballotlem2  23063  or3di  23139  eliccelico  23285  relogbcl  23419  prob01  23631  probun  23637  pconcon  23777  rescon  23792  iscvm  23805  cvmlift2lem12  23860  cvmlift3lem5  23869  lediv2aALT  24028  dfso3  24089  divelunit  24095  br6  24185  preduz  24271  nofulllem2  24428  nofulllem5  24431  brsuccf  24551  axeuclidlem  24662  axeuclid  24663  cgrxfr  24750  segcon2  24800  seglecgr12im  24805  seglecgr12  24806  segletr  24809  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsidele  24827  itg2addnclem  25003  eqvinopb  25068  copsexgb  25069  elo  25144  dff1o6f  25195  prismorcsetlem  26015  prismorcset  26017  prismorcsetlemc  26020  cmppar  26076  cmppar3  26077  isibcg  26294  fdc  26558  isbnd3b  26612  ablo4pnp  26673  crngm4  26731  isidlc  26743  pridl  26765  ispridl2  26766  ispridlc  26798  3anrabdioph  26965  issdrg2  27609  fgraphxp  27633  rfcnnnub  27810  stoweidlem35  27887  ndmaovass  28174  nb3grapr2  28290  nb3gra2nb  28291  trlonprop  28341  0wlk  28343  0trl  28344  3v3e3cycl1  28390  frgra3v  28426  1to3vfriswmgra  28431  dfvd3  28659  3impexpVD  28948  bnj170  29039  bnj248  29041  bnj252  29044  bnj253  29045  bnj945  29121  bnj1098  29131  bnj1224  29150  bnj150  29224  bnj153  29228  bnj545  29243  bnj557  29249  bnj571  29254  bnj594  29260  bnj864  29270  bnj865  29271  bnj849  29273  bnj964  29291  bnj986  29302  bnj996  29303  bnj1033  29315  bnj1110  29328  bnj1128  29336  bnj1174  29349  sb3anNEW7  29611  eeeanvOLD7  29658  islshpsm  29792  islshpat  29829  cmtfvalN  30022  cmtvalN  30023  ishlat1  30164  ishlat2  30165  3dim0  30268  2dim  30281  islvol5  30390  lhpexle3  30823  cdleme0ex2N  31035  cdleme0nex  31101  cdlemg2cex  31402  cdlemg33b0  31512  cdlemg33b  31518  cdlemg33c  31519  cdlemg33e  31521  dib1dim  31977  diblsmopel  31983  dihopelvalcpre  32060  lcfls1c  32348
  Copyright terms: Public domain W3C validator