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

Definition df-3an 869
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 867 . 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  871  3anrot  872  3ancoma  874  3anan32  878  3ioran  882  3simpa  883  3pm3.2i  1064  pm3.2an3  1065  3jca  1066  3anbi123i  1074  3imp  1079  3anbi123d  1188  3anim123d  1195  an6  1197  19.26-3an  1346  hb3an  1416  nf3an  1432  nf3and  1435  eeeanv  1782  sb3an  1806  mopick2  1957  r19.26-3  2413  3reeanv  2450  ceqsex3v  2565  ceqsex4v  2566  ceqsex8v  2568  elin3  3097  raltpg  3387  tpss  3493  dfopg  3511  opeq1  3513  opeq2  3514  opm  3935  otth2  3942  poirr  4008  po3nr  4011  rabxp  4296  brinxp2  4323  brinxp  4324  sotri2  4638  sotri3  4639  f1orn  5050  dff1o6  5330  isosolem  5377  oprabid  5450  caovimo  5606  elovmpt2  5613  dfxp3  5732  nnaord  5982  prmuloc  6397  ltrelxr  6681  ltxr  8172  bd3an  8287
  Copyright terms: Public domain W3C validator