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

Definition df-3an 949
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 947 . 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  951  3anrot  952  3ancoma  954  3anan32  958  3ioran  962  3simpa  963  3pm3.2i  1144  pm3.2an3  1145  3jca  1146  3anbi123i  1155  3imp  1160  3anbi123d  1275  3anim123d  1282  an6  1284  19.26-3an  1444  hb3an  1514  nf3an  1530  nf3and  1533  eeeanv  1885  sb3an  1909  mopick2  2060  r19.26-3  2539  3reeanv  2578  ceqsex3v  2702  ceqsex4v  2703  ceqsex8v  2705  sbc3an  2942  elin3  3237  raltpg  3546  tpss  3655  dfopg  3673  opeq1  3675  opeq2  3676  opm  4126  otth2  4133  poirr  4199  po3nr  4202  wepo  4251  wetrep  4252  rabxp  4546  brinxp2  4576  brinxp  4577  sotri2  4906  sotri3  4907  f1orn  5345  dff1o6  5645  isosolem  5693  oprabid  5771  caovimo  5932  elovmpo  5939  dfxp3  6060  nnaord  6373  fiintim  6785  prmuloc  7342  ltrelxr  7793  rexuz2  9332  ltxr  9517  elixx3g  9639  elioo4g  9672  elioopnf  9705  elioomnf  9706  elicopnf  9707  elxrge0  9716  divelunit  9740  elfz2  9752  elfzuzb  9755  uzsplit  9827  fznn0  9848  elfzmlbp  9864  elfzo2  9882  fzolb2  9886  fzouzsplit  9911  ssfzo12bi  9957  fzind2  9971  abs2dif  10833  sumeq2  11083  divalgb  11534  divgcdz  11572  rplpwr  11627  cncongr1  11696  isbasis3g  12124  lmfval  12272  lmbr  12293  lmbr2  12294  xmeterval  12515  xmeter  12516  cnbl0  12614  cnblcld  12615  limcrcl  12707  bd3an  12924
  Copyright terms: Public domain W3C validator