ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-3an Structured version   GIF version

Definition df-3an 886
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 381. (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 884 . 2 wff (φ ψ χ)
51, 2wa 97 . . 3 wff (φ ψ)
65, 3wa 97 . 2 wff ((φ ψ) χ)
74, 6wb 98 1 wff ((φ ψ χ) ↔ ((φ ψ) χ))
Colors of variables: wff set class
This definition is referenced by:  3anass  888  3anrot  889  3ancoma  891  3anan32  895  3ioran  899  3simpa  900  3pm3.2i  1081  pm3.2an3  1082  3jca  1083  3anbi123i  1092  3imp  1097  3anbi123d  1206  3anim123d  1213  an6  1215  19.26-3an  1369  hb3an  1439  nf3an  1455  nf3and  1458  eeeanv  1805  sb3an  1829  mopick2  1980  r19.26-3  2437  3reeanv  2474  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  elin3  3122  raltpg  3414  tpss  3520  dfopg  3538  opeq1  3540  opeq2  3541  opm  3962  otth2  3969  poirr  4035  po3nr  4038  rabxp  4323  brinxp2  4350  brinxp  4351  sotri2  4665  sotri3  4666  f1orn  5079  dff1o6  5359  isosolem  5406  oprabid  5480  caovimo  5636  elovmpt2  5643  dfxp3  5762  nnaord  6018  prmuloc  6546  ltrelxr  6857  rexuz2  8280  ltxr  8445  elixx3g  8520  elioo4g  8553  elioopnf  8586  elioomnf  8587  elicopnf  8588  elxrge0  8597  divelunit  8620  elfz2  8631  elfzuzb  8634  uzsplit  8704  fznn0  8724  elfzmlbp  8740  elfzo2  8757  fzolb2  8760  fzouzsplit  8785  ssfzo12bi  8831  fzind2  8845  bd3an  9265
  Copyright terms: Public domain W3C validator