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

Definition df-3an 973
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 647. (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 971 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 367 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 367 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 184 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff setvar class
This definition is referenced by:  3anass  975  3anrot  976  3ancoma  978  3anan32  983  3anor  987  3ioran  989  3simpa  991  3pm3.2i  1172  pm3.2an3  1173  3jca  1174  3anbi123i  1183  3imp  1188  3an4anass  1217  3anbi123d  1297  3anim123d  1304  an6  1306  an3andi  1339  an33rean  1340  cadan  1466  19.26-3an  1690  4exdistr  1789  nf3and  1934  nf3an  1938  eeeanv  1997  sb3an  2145  mopick2  2293  r3al  2762  r19.26-3  2911  3reeanv  2951  ceqsex3v  3074  ceqsex4v  3075  ceqsex8v  3077  sbc3an  3310  elin3  3604  raltpg  3995  tpss  4109  dfopif  4128  disjxun  4365  otth2  4643  otthg  4645  oteqex  4654  poirr  4725  po3nr  4728  wefrc  4787  rabxp  4950  brinxp2  4975  brinxp  4976  f1orn  5734  dff1o6  6082  oprabid  6223  oprabv  6244  ndmovass  6362  elovmpt2  6419  elovmpt2rab  6420  elovmpt2rab1  6421  elovmpt3rab1  6435  dfwe2  6516  opiota  6758  dfxp3  6759  bropopvvv  6779  oaord  7114  oeeu  7170  nnaord  7186  swoso  7260  fiint  7712  funsnfsupp  7768  alephval3  8404  fpwwe2lem8  8926  fpwwe2lem9  8927  fpwwe2lem12  8930  ingru  9104  axgroth3  9120  ltrelxr  9559  ltxrlt  9566  wloglei  10002  sup2  10415  rexuz2  11052  ltxr  11245  elixx3g  11463  ixxun  11466  elioo4g  11506  elioopnf  11539  elioomnf  11540  elicopnf  11541  elxrge0  11550  divelunit  11583  elfz2  11600  elfzuzb  11603  uzsplit  11672  fznn0  11692  elfzmlbp  11708  elfzo2  11725  fzolb2  11729  fzouzsplit  11755  ssfzo12bi  11806  fzind2  11823  ccatsymb  12509  swrdsbslen  12584  swrdspsleq  12585  swrdccatin2  12623  swrdccatin12lem2  12625  swrdccatin12lem3  12626  swrdccatin12  12627  repsdf2  12661  repswsymball  12662  repswsymballbi  12663  repswswrd  12667  abs2dif  13167  sinltx  13926  divalglem8  14060  divalglem10  14062  divalgb  14064  bitsval2  14077  rplpwr  14196  pythagtriplem2  14343  pythagtrip  14360  pwsle  14899  imasvscafn  14944  mreexmrid  15050  iscatd2  15088  issect  15159  issect2  15160  oppcsect  15184  isfunc  15270  funcpropd  15306  fucsect  15378  fucinv  15379  initoeu2  15412  setcsect  15485  setcinv  15486  issubm2  16096  issubg3  16336  resgrpisgrp  16339  cycsubgcl  16344  eqgval  16367  eqger  16368  isgim  16427  gaorb  16462  gaorber  16463  gastacos  16465  symg2bas  16540  galactghm  16545  gsmsymgreqlem2  16573  pmtr3ncom  16617  ispgp  16729  efgcpbllema  16889  efgcpbllemb  16890  eqgabl  16960  dprdw  17156  dprdwOLD  17163  ringpropd  17343  ringrghm  17364  isirred2  17463  rim0to0  17504  drngid2  17525  islss  17694  islmim  17821  lmhmpropd  17832  isassa  18077  mpfrcl  18300  zndvds  18679  znleval  18684  znleval2  18685  obselocv  18850  matinvgcell  19022  mat1dimscm  19062  scmatscm  19100  scmatf1  19118  mdetunilem7  19205  cpmatacl  19302  cpmatmcl  19305  mat2pmatf1  19315  mat2pmatghm  19316  mat2pmatmul  19317  mat2pmatlin  19321  mat2pmatscmxcl  19326  m2pmfzgsumcl  19334  decpmataa0  19354  monmatcollpw  19365  pmatcollpwscmatlem1  19375  pmatcollpwscmatlem2  19376  pm2mpghm  19402  pm2mpmhmlem2  19405  monmat2matmon  19410  chfacfisf  19440  chfacfisfcpmat  19441  chfacfpmmulgsum2  19451  isbasis3g  19535  leordtvallem2  19798  lmfval  19819  lmbr  19845  lmbr2  19846  lmmo  19967  dfcon2  20005  ptbasin  20163  ptbasfi  20167  txcnpi  20194  ptcnp  20208  hausdiag  20231  qtophmeo  20403  fbunfip  20455  elflim2  20550  hausflimi  20566  isfcls  20595  isfcls2  20599  istmd  20658  istgp  20661  istrg  20751  istdrg  20753  istdrg2  20765  istlm  20772  imasdsf1olem  20961  xmeterval  21020  xmeter  21021  prdsxmslem2  21117  blval2  21163  isngp  21201  isngp2  21202  isngp3  21203  isnlm  21269  cnbl0  21366  cnblcld  21367  elii1  21520  isphtpc  21579  phtpcer  21580  iscph  21702  lmmbr  21782  lmmbr2  21783  lmmbrf  21786  iscfil2  21790  iscau3  21802  iscau4  21803  iscauf  21804  caucfil  21807  isbn  21862  ishl2  21895  ovolfcl  21963  ioombl1lem4  22056  mbfmax  22141  iblpos  22284  limcrcl  22363  ig1pval3  22660  ulmdvlem3  22882  ellogdm  23107  relogbcl  23231  fsumvma2  23606  chpchtsum  23611  chpub  23612  dchrelbas3  23630  axeuclidlem  24386  axeuclid  24387  nb3grapr2  24575  nb3gra2nb  24576  0wlk  24668  0trl  24669  constr2wlk  24721  3v3e3cycl1  24765  wwlknred  24844  wwlknndef  24858  isclwlk  24877  clwwlkprop  24891  clwwlknndef  24894  clwwlknwwlkncl  24921  wwlkext2clwwlk  24924  wwlksubclwwlk  24925  clwwnisshclwwn  24930  erclwwlkref  24934  erclwwlknref  24946  clwlkfoclwwlk  24966  el2wlkonotot0  24993  el2wlkonotot  24994  el2wlkonotot1  24995  2wlkonotv  24998  usg2spthonot0  25010  cusgraisrusgra  25059  rusgranumwlkl1  25068  rusgranumwlkb0  25074  rusgra0edg  25076  rusgranumwlk  25078  frgra3v  25123  1to3vfriswmgra  25128  frgraregorufrg  25193  extwwlkfablem2  25199  numclwwlkffin  25203  numclwwlkovfel2  25204  numclwwlkovf2  25205  numclwwlkovf2ex  25207  numclwwlkovgelim  25210  numclwlk1lem2fo  25216  numclwwlk2lem1  25223  numclwwlk7  25235  nvex  25621  isnv  25622  dfadj2  26920  cnvadj  26927  adjeq  26970  eleigvec  26992  eleigvec2  26993  chirredi  27429  or3di  27484  dfrp2  27734  eliccelico  27741  omndmul2  27855  isorng  27943  eulerpartlemv  28486  eulerpartlemd  28488  eulerpartlemn  28503  prob01  28535  probun  28541  pconcon  28865  rescon  28880  iscvm  28893  cvmlift2lem12  28948  cvmlift3lem5  28957  elmpst  29085  mpstrcl  29090  lediv2aALT  29232  dfso3  29263  br6  29352  preduz  29445  nofulllem2  29628  nofulllem5  29631  elfuns  29718  brimg  29740  brsuccf  29744  cgrxfr  29858  segcon2  29908  seglecgr12im  29913  seglecgr12  29914  segletr  29917  btwnoutside  29928  broutsideof3  29929  outsideoftr  29932  outsidele  29935  fdc  30404  isbnd3b  30447  ablo4pnp  30508  crngm4  30566  isidlc  30578  pridl  30600  ispridl2  30601  ispridlc  30633  ts3an1  30723  ts3an2  30724  ts3an3  30725  3anrabdioph  30881  issdrg2  31315  fgraphxp  31339  rfcnnnub  31578  stoweidlem35  31983  ndmaovass  32457  pfxccatin12lem2  32599  pfxccatin12  32600  pfxccat3a  32604  rexdifpr  32621  elfz2z  32652  usgra2pth0  32673  ismhm0  32811  rnglz  32890  rngcsect  32988  rngcinv  32989  rngcsectALTV  33000  rngcinvALTV  33001  ringcsect  33039  ringcinv  33040  ringcsectALTV  33063  ringcinvALTV  33064  islindeps  33254  islindeps2  33284  isldepslvec2  33286  elbigo2  33373  dfvd3  33708  3impexpVD  34002  bnj170  34097  bnj248  34099  bnj252  34102  bnj253  34103  bnj945  34179  bnj1098  34189  bnj1224  34207  bnj150  34281  bnj153  34285  bnj545  34300  bnj557  34306  bnj571  34311  bnj594  34317  bnj864  34327  bnj865  34328  bnj849  34330  bnj964  34348  bnj986  34359  bnj996  34360  bnj1033  34372  bnj1110  34385  bnj1128  34393  bnj1174  34406  bj-imn3ani  34523  islshpsm  35118  islshpat  35155  cmtfvalN  35348  cmtvalN  35349  ishlat1  35490  ishlat2  35491  3dim0  35594  2dim  35607  islvol5  35716  lhpexle3  36149  cdleme0ex2N  36362  cdleme0nex  36428  cdlemg2cex  36730  cdlemg33b0  36840  cdlemg33b  36846  cdlemg33c  36847  cdlemg33e  36849  dib1dim  37305  diblsmopel  37311  dihopelvalcpre  37388  lcfls1c  37676
  Copyright terms: Public domain W3C validator