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

Definition df-3an 924
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 393. (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 922 . 2 wff (𝜑𝜓𝜒)
51, 2wa 102 . . 3 wff (𝜑𝜓)
65, 3wa 102 . 2 wff ((𝜑𝜓) ∧ 𝜒)
74, 6wb 103 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3anass  926  3anrot  927  3ancoma  929  3anan32  933  3ioran  937  3simpa  938  3pm3.2i  1119  pm3.2an3  1120  3jca  1121  3anbi123i  1130  3imp  1135  3anbi123d  1246  3anim123d  1253  an6  1255  19.26-3an  1415  hb3an  1485  nf3an  1501  nf3and  1504  eeeanv  1853  sb3an  1877  mopick2  2028  r19.26-3  2495  3reeanv  2533  ceqsex3v  2655  ceqsex4v  2656  ceqsex8v  2658  sbc3an  2889  elin3  3180  raltpg  3478  tpss  3585  dfopg  3603  opeq1  3605  opeq2  3606  opm  4035  otth2  4042  poirr  4108  po3nr  4111  wepo  4160  wetrep  4161  rabxp  4446  brinxp2  4473  brinxp  4474  sotri2  4796  sotri3  4797  f1orn  5226  dff1o6  5516  isosolem  5564  oprabid  5638  caovimo  5795  elovmpt2  5802  dfxp3  5921  nnaord  6220  prmuloc  7069  ltrelxr  7491  rexuz2  9001  ltxr  9178  elixx3g  9251  elioo4g  9284  elioopnf  9317  elioomnf  9318  elicopnf  9319  elxrge0  9328  divelunit  9351  elfz2  9363  elfzuzb  9366  uzsplit  9436  fznn0  9457  elfzmlbp  9471  elfzo2  9489  fzolb2  9493  fzouzsplit  9518  ssfzo12bi  9564  fzind2  9578  abs2dif  10435  sumeq2  10640  divalgb  10807  divgcdz  10845  rplpwr  10898  cncongr1  10967  bd3an  11166
  Copyright terms: Public domain W3C validator