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

Definition df-3an 1032
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 678. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3an ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
3 wch . . 3 wff 𝜒
41, 2, 3w3a 1030 . 2 wff (𝜑𝜓𝜒)
51, 2wa 382 . . 3 wff (𝜑𝜓)
65, 3wa 382 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 194 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3anass  1034  3anrot  1035  3ancoma  1037  3anan32  1042  3anor  1046  3ioran  1048  3simpa  1050  3pm3.2i  1231  pm3.2an3  1232  pm3.2an3OLD  1233  3jca  1234  3anbi123i  1243  3imp  1248  3an4anass  1282  3anbi123d  1390  3anim123d  1397  an6  1399  an3andi  1436  an33rean  1437  cadan  1538  19.26-3an  1787  nf3and  1814  nf3an  1818  4exdistr  1910  eeeanv  2170  nf3andOLD  2220  nf3anOLD  2226  sb3an  2387  mopick2  2527  r3al  2923  r19.26-3  3047  3reeanv  3086  ceqsex3v  3218  ceqsex4v  3219  ceqsex8v  3221  sbc3an  3460  elin3  3765  raltpg  4182  tpss  4303  dfopif  4331  disjxun  4575  otth2  4871  otthg  4873  oteqex  4882  poirr  4959  po3nr  4962  wefrc  5021  rabxp  5067  brinxp2  5092  brinxp  5093  f1orn  6044  dff1o6  6408  oprabid  6553  oprabv  6578  ndmovass  6697  elovmpt2  6754  elovmpt2rab  6755  elovmpt2rab1  6756  elovmpt3rab1  6768  dfwe2  6850  opiota  7095  dfxp3  7096  bropopvvv  7119  oaord  7491  oeeu  7547  nnaord  7563  swoso  7639  fiint  8099  funsnfsupp  8159  alephval3  8793  fpwwe2lem8  9315  fpwwe2lem9  9316  fpwwe2lem12  9319  ingru  9493  axgroth3  9509  ltrelxr  9950  ltxrlt  9959  wloglei  10411  sup2  10830  rexuz2  11573  ltxr  11786  elixx3g  12017  ixxun  12020  elioo4g  12063  elioopnf  12096  elioomnf  12097  elicopnf  12098  elxrge0  12110  divelunit  12143  elfz2  12161  elfzuzb  12164  uzsplit  12238  fznn0  12258  elfzmlbp  12276  preduz  12287  elfzo2  12299  fzolb2  12303  fzouzsplit  12329  ssfzo12bi  12386  fzind2  12405  ccatsymb  13167  swrdsbslen  13248  swrdspsleq  13249  swrdccatin2  13286  swrdccatin12lem2  13288  swrdccatin12lem3  13289  swrdccatin12  13290  repsdf2  13324  repswsymball  13325  repswsymballbi  13326  repswswrd  13330  wrdl3s3  13501  s3sndisj  13502  s3iunsndisj  13503  abs2dif  13868  sinltx  14706  divalglem8  14909  divalglem10  14911  divalgb  14913  bitsval2  14933  divgcdz  15019  rplpwr  15062  cncongr1  15167  pythagtriplem2  15308  pythagtrip  15325  prmgaplem4  15544  pwsle  15923  imasvscafn  15968  mreexmrid  16074  iscatd2  16113  issect  16184  issect2  16185  oppcsect  16209  isfunc  16295  funcpropd  16331  fucsect  16403  fucinv  16404  initoeu2  16437  setcsect  16510  setcinv  16511  issubm2  17119  issubg3  17383  resgrpisgrp  17386  cycsubgcl  17391  eqgval  17414  eqger  17415  isgim  17475  gaorb  17511  gaorber  17512  gastacos  17514  symg2bas  17589  galactghm  17594  gsmsymgreqlem2  17622  pmtr3ncom  17666  ispgp  17778  efgcpbllema  17938  efgcpbllemb  17939  eqgabl  18011  dprdw  18180  ringpropd  18353  ringrghm  18376  isirred2  18472  rim0to0  18513  drngid2  18534  islss  18704  islmim  18831  lmhmpropd  18842  isassa  19084  mpfrcl  19287  zndvds  19664  znleval  19669  znleval2  19670  obselocv  19838  matinvgcell  20007  mat1dimscm  20047  scmatscm  20085  scmatf1  20103  mdetunilem7  20190  cpmatacl  20287  cpmatmcl  20290  mat2pmatf1  20300  mat2pmatghm  20301  mat2pmatmul  20302  mat2pmatlin  20306  mat2pmatscmxcl  20311  m2pmfzgsumcl  20319  decpmataa0  20339  monmatcollpw  20350  pmatcollpwscmatlem1  20360  pmatcollpwscmatlem2  20361  pm2mpghm  20387  pm2mpmhmlem2  20390  monmat2matmon  20395  chfacfisf  20425  chfacfisfcpmat  20426  chfacfpmmulgsum2  20436  isbasis3g  20511  leordtvallem2  20772  lmfval  20793  lmbr  20819  lmbr2  20820  lmmo  20941  dfcon2  20979  ptbasin  21137  ptbasfi  21141  txcnpi  21168  ptcnp  21182  hausdiag  21205  qtophmeo  21377  fbunfip  21430  elflim2  21525  hausflimi  21541  isfcls  21570  isfcls2  21574  istmd  21635  istgp  21638  istrg  21724  istdrg  21726  istdrg2  21738  istlm  21745  imasdsf1olem  21935  xmeterval  21994  xmeter  21995  prdsxmslem2  22091  blval2  22124  isngp  22157  isngp2  22158  isngp3  22159  isnlm  22236  cnbl0  22334  cnblcld  22335  elii1  22489  isphtpc  22548  phtpcer  22549  phtpcerOLD  22550  isclmp  22652  iscph  22722  lmmbr  22808  lmmbr2  22809  lmmbrf  22812  iscfil2  22816  iscau3  22828  iscau4  22829  iscauf  22830  caucfil  22833  isbn  22887  ishl2  22918  ovolfcl  22986  ioombl1lem4  23080  mbfmax  23166  iblpos  23309  limcrcl  23388  ig1pval3  23682  ulmdvlem3  23904  ellogdm  24129  relogbcl  24255  fsumvma2  24683  chpchtsum  24688  chpub  24689  dchrelbas3  24707  gausslemma2dlem1a  24834  lnhl  25255  colopp  25406  dfcgra2  25466  axeuclidlem  25587  axeuclid  25588  nb3grapr2  25776  nb3gra2nb  25777  0wlk  25868  0trl  25869  constr2wlk  25921  3v3e3cycl1  25965  wwlknred  26044  wwlknndef  26058  isclwlk  26077  clwwlkprop  26091  clwwlknndef  26094  clwwlknwwlkncl  26121  wwlkext2clwwlk  26124  wwlksubclwwlk  26125  clwwnisshclwwn  26130  erclwwlkref  26134  erclwwlknref  26146  clwlkfoclwwlk  26165  el2wlkonotot0  26192  el2wlkonotot  26193  el2wlkonotot1  26194  2wlkonotv  26197  usg2spthonot0  26209  cusgraisrusgra  26258  rusgranumwlkl1  26267  rusgranumwlkb0  26273  rusgra0edg  26275  rusgranumwlk  26277  frgra3v  26322  1to3vfriswmgra  26327  frgraregorufrg  26392  extwwlkfablem2  26398  numclwwlkffin  26402  numclwwlkovfel2  26403  numclwwlkovf2  26404  numclwwlkovf2ex  26406  numclwwlkovgelim  26409  numclwlk1lem2fo  26415  numclwwlk2lem1  26422  numclwwlk7  26434  nvex  26643  isnv  26644  dfadj2  27921  cnvadj  27928  adjeq  27971  eleigvec  27993  eleigvec2  27994  chirredi  28430  or3di  28484  dfrp2  28715  eliccelico  28722  omndmul2  28836  isorng  28923  pmtrprfv2  28972  fzto1st  28977  psgnfzto1st  28979  eulerpartlemv  29546  eulerpartlemd  29548  eulerpartlemn  29563  prob01  29595  probun  29601  bnj170  29810  bnj248  29812  bnj252  29815  bnj253  29816  bnj945  29891  bnj1098  29901  bnj1224  29919  bnj150  29993  bnj153  29997  bnj545  30012  bnj557  30018  bnj571  30023  bnj594  30029  bnj864  30039  bnj865  30040  bnj849  30042  bnj964  30060  bnj986  30071  bnj996  30072  bnj1033  30084  bnj1110  30097  bnj1128  30105  bnj1174  30118  pconcon  30260  rescon  30275  iscvm  30288  cvmlift2lem12  30343  cvmlift3lem5  30352  elmpst  30480  mpstrcl  30485  lediv2aALT  30618  dfso3  30649  br6  30693  nofulllem2  30895  nofulllem5  30898  elfuns  30985  brimg  31007  brsuccf  31011  cgrxfr  31125  segcon2  31175  seglecgr12im  31180  seglecgr12  31181  segletr  31184  btwnoutside  31195  broutsideof3  31196  outsideoftr  31199  outsidele  31202  bj-imn3ani  31538  relowlpssretop  32171  lindsenlbs  32357  matunitlindflem2  32359  fdc  32494  isbnd3b  32537  ablo4pnp  32632  crngm4  32755  isidlc  32767  pridl  32789  ispridl2  32790  ispridlc  32822  ts3an1  32910  ts3an2  32911  ts3an3  32912  islshpsm  33068  islshpat  33105  cmtfvalN  33298  cmtvalN  33299  ishlat1  33440  ishlat2  33441  3dim0  33544  2dim  33557  islvol5  33666  lhpexle3  34099  cdleme0ex2N  34312  cdleme0nex  34378  cdlemg2cex  34680  cdlemg33b0  34790  cdlemg33b  34796  cdlemg33c  34797  cdlemg33e  34799  dib1dim  35255  diblsmopel  35261  dihopelvalcpre  35338  lcfls1c  35626  3anrabdioph  36147  issdrg2  36570  fgraphxp  36591  dfrtrcl5  36738  brfvrcld2  36786  df3an2  36863  dfvd3  37611  3impexpVD  37896  rfcnnnub  38001  stoweidlem35  38711  smflimlem4  39443  ndmaovass  39719  nltle2tri  39726  gboage9  39970  sgoldbalt  39987  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  bgoldbtbndlem4  40008  bgoldbtbnd  40009  pfxccatin12lem2  40071  pfxccatin12  40072  pfxccat3a  40076  rexdifpr  40100  fpropnf1  40143  elfz2z  40158  edgupgr  40348  umgr2edg1  40419  subusgr  40494  nb3grpr2  40592  nb3gr2nb  40593  isuvtxa  40602  nbupgruvtxres  40615  iscplgredg  40620  cplgr3v  40638  rusgrpropedg  40765  rgrusgrprc  40770  rusgrprc  40771  wlkOnprop  40847  lfgriswlk  40878  1wlksonproplem  40893  usgr2pth0  40952  isclWlke  40965  crctcshtrl  41007  iswwlksnx  41023  wwlknbp  41025  2trld  41126  rusgrnumwwlkl1  41153  rusgrnumwwlkb0  41155  rusgrnumwwlk  41159  erclwwlksref  41222  erclwwlksnref  41234  clwlksf1clwwlklem0  41252  01wlk  41265  3spthd  41324  umgr3v3e3cycl  41332  frgr3v  41426  1to3vfriswmgr  41431  frgr2wwlkeu  41473  av-extwwlkfablem2  41491  av-numclwwlkovfel2  41495  av-numclwwlkovf2  41496  av-numclwlk1lem2fo  41506  ismhm0  41576  rnglz  41655  rngcsect  41753  rngcinv  41754  rngcsectALTV  41765  rngcinvALTV  41766  ringcsect  41804  ringcinv  41805  ringcsectALTV  41828  ringcinvALTV  41829  islindeps  42017  islindeps2  42047  isldepslvec2  42049  elbigo2  42125
  Copyright terms: Public domain W3C validator