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  1392  19.26-3an  1595  nf3and  1827  nf3an  1832  hb3anOLD  1836  eeeanv  1919  sb3an  2075  mopick2  2276  r19.26-3  2753  3reeanv  2784  ceqsex3v  2902  ceqsex4v  2903  ceqsex8v  2905  elin3  3436  raltpg  3760  tpss  3858  dfopif  3872  disjxun  4100  otth2  4328  oteqex  4338  poirr  4404  po3nr  4407  wefrc  4466  dfwe2  4652  rabxp  4804  brinxp2  4830  brinxp  4831  f1orn  5562  dff1o6  5875  oprabid  5966  ndmovass  6092  elovmpt2  6148  dfxp3  6263  opiota  6374  oaord  6629  oeeui  6684  oeeu  6685  nnaord  6701  swoso  6775  fiint  7220  alephval3  7824  fpwwe2lem8  8346  fpwwe2lem9  8347  fpwwe2lem12  8350  ingru  8524  axgroth3  8540  ltrelxr  8973  ltxrlt  8980  wloglei  9392  sup2  9797  rexuz2  10359  ltxr  10546  elixx3g  10758  ixxun  10761  elioo4g  10800  elioopnf  10826  elioomnf  10827  elicopnf  10828  elxrge0  10836  elfz2  10878  elfzuzb  10881  fznn0  10940  uzsplit  10944  elfzo2  10967  fzolb2  10970  fzouzsplit  10990  fzind2  11012  abs2dif  11906  sinltx  12560  divalglem8  12690  divalglem10  12692  divalgb  12694  bitsval2  12707  rplpwr  12826  pythagtriplem2  12961  pythagtrip  12978  pwsle  13484  imasvscafn  13532  mreexmrid  13638  iscatd2  13676  issect  13749  issect2  13750  oppcsect  13769  isfunc  13831  funcpropd  13867  fucsect  13939  fucinv  13940  setcsect  14014  setcinv  14015  mndcl  14465  issubm2  14519  issubg3  14730  cycsubgcl  14736  eqgval  14759  eqger  14760  isgim  14819  gaorb  14854  gaorber  14855  gastacos  14857  galactghm  14876  ispgp  14996  efgcpbllema  15156  efgcpbllemb  15157  eqgabl  15224  dprdw  15338  rngpropd  15465  rngrghm  15482  isirred2  15576  drngid2  15621  islss  15785  islmim  15908  lmhmpropd  15919  isassa  16149  zndvds  16603  znleval  16608  znleval2  16609  obselocv  16728  isbasis3g  16787  leordtvallem2  17041  lmfval  17062  lmbr  17088  lmbr2  17089  lmmo  17208  dfcon2  17245  ptbasin  17372  ptbasfi  17376  txcnpi  17402  ptcnp  17416  hausdiag  17439  qtophmeo  17608  fbunfip  17660  elflim2  17755  hausflimi  17771  isfcls  17800  isfcls2  17804  istmd  17853  istgp  17856  istrg  17942  istdrg  17944  istdrg2  17956  istlm  17963  imasdsf1olem  18033  xmeterval  18074  xmeter  18075  prdsxmslem2  18171  isngp  18214  isngp2  18215  isngp3  18216  isnlm  18282  cnbl0  18379  cnblcld  18380  elii1  18531  isphtpc  18590  phtpcer  18591  iscph  18704  lmmbr  18782  lmmbr2  18783  lmmbrf  18786  iscfil2  18790  iscau3  18802  iscau4  18803  iscauf  18804  caucfil  18807  isbn  18858  ishl2  18885  ovolfcl  18924  ioombl1lem4  19016  mbfmax  19102  iblpos  19245  limcrcl  19322  mpfrcl  19500  ig1pval3  19658  ulmdvlem3  19879  ellogdm  20091  fsumvma2  20559  chpchtsum  20564  chpub  20565  dchrelbas3  20583  nvex  21275  isnv  21276  dfadj2  22573  cnvadj  22580  adjeq  22623  eleigvec  22645  eleigvec2  22646  chirredi  23082  or3di  23138  eliccelico  23339  blval2  23608  relogbcl  23668  prob01  23920  probun  23926  ballotlem2  23995  pconcon  24166  rescon  24181  iscvm  24194  cvmlift2lem12  24249  cvmlift3lem5  24258  lediv2aALT  24417  dfso3  24478  divelunit  24486  br6  24672  preduz  24758  nofulllem2  24915  nofulllem5  24918  brsuccf  25038  axeuclidlem  25149  axeuclid  25150  cgrxfr  25237  segcon2  25287  seglecgr12im  25292  seglecgr12  25293  segletr  25296  btwnoutside  25307  broutsideof3  25308  outsideoftr  25311  outsidele  25314  itg2addnclem  25492  fdc  25779  isbnd3b  25832  ablo4pnp  25893  crngm4  25951  isidlc  25963  pridl  25985  ispridl2  25986  ispridlc  26018  3anrabdioph  26185  issdrg2  26829  fgraphxp  26853  rfcnnnub  27030  stoweidlem35  27107  ndmaovass  27394  bropopvvv  27432  nb3grapr2  27609  nb3gra2nb  27610  0wlk  27680  0trl  27681  3v3e3cycl1  27751  frgra3v  27818  1to3vfriswmgra  27823  dfvd3  28088  3impexpVD  28377  bnj170  28468  bnj248  28470  bnj252  28473  bnj253  28474  bnj945  28550  bnj1098  28560  bnj1224  28579  bnj150  28653  bnj153  28657  bnj545  28672  bnj557  28678  bnj571  28683  bnj594  28689  bnj864  28699  bnj865  28700  bnj849  28702  bnj964  28720  bnj986  28731  bnj996  28732  bnj1033  28744  bnj1110  28757  bnj1128  28765  bnj1174  28778  sb3anNEW7  29041  eeeanvOLD7  29088  islshpsm  29222  islshpat  29259  cmtfvalN  29452  cmtvalN  29453  ishlat1  29594  ishlat2  29595  3dim0  29698  2dim  29711  islvol5  29820  lhpexle3  30253  cdleme0ex2N  30465  cdleme0nex  30531  cdlemg2cex  30832  cdlemg33b0  30942  cdlemg33b  30948  cdlemg33c  30949  cdlemg33e  30951  dib1dim  31407  diblsmopel  31413  dihopelvalcpre  31490  lcfls1c  31778
  Copyright terms: Public domain W3C validator