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

Definition df-3an 964
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 398. (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 962 . 2 wff (𝜑𝜓𝜒)
51, 2wa 103 . . 3 wff (𝜑𝜓)
65, 3wa 103 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 104 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3anass  966  3anrot  967  3ancoma  969  3anan32  973  3ioran  977  3simpa  978  3pm3.2i  1159  pm3.2an3  1160  3jca  1161  3anbi123i  1170  3imp  1175  3anbi123d  1290  3anim123d  1297  an6  1299  19.26-3an  1459  hb3an  1529  nf3an  1545  nf3and  1548  eeeanv  1905  sb3an  1931  mopick2  2082  r19.26-3  2562  3reeanv  2601  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  sbc3an  2970  elin3  3267  raltpg  3576  tpss  3685  dfopg  3703  opeq1  3705  opeq2  3706  opm  4156  otth2  4163  poirr  4229  po3nr  4232  wepo  4281  wetrep  4282  rabxp  4576  brinxp2  4606  brinxp  4607  sotri2  4936  sotri3  4937  f1orn  5377  dff1o6  5677  isosolem  5725  oprabid  5803  caovimo  5964  elovmpo  5971  dfxp3  6092  nnaord  6405  fiintim  6817  prmuloc  7381  ltrelxr  7832  rexuz2  9383  ltxr  9569  elixx3g  9691  elioo4g  9724  elioopnf  9757  elioomnf  9758  elicopnf  9759  elxrge0  9768  divelunit  9792  elfz2  9804  elfzuzb  9807  uzsplit  9879  fznn0  9900  elfzmlbp  9916  elfzo2  9934  fzolb2  9938  fzouzsplit  9963  ssfzo12bi  10009  fzind2  10023  abs2dif  10885  sumeq2  11135  divalgb  11628  divgcdz  11666  rplpwr  11721  cncongr1  11790  isbasis3g  12222  lmfval  12370  lmbr  12391  lmbr2  12392  xmeterval  12613  xmeter  12614  cnbl0  12712  cnblcld  12713  limcrcl  12805  bd3an  13081
  Copyright terms: Public domain W3C validator