ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-3an Unicode 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  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)

Detailed syntax breakdown of Definition df-3an
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3w3a 922 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 102 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 102 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 103 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
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  3480  tpss  3587  dfopg  3605  opeq1  3607  opeq2  3608  opm  4037  otth2  4044  poirr  4110  po3nr  4113  wepo  4162  wetrep  4163  rabxp  4448  brinxp2  4475  brinxp  4476  sotri2  4798  sotri3  4799  f1orn  5228  dff1o6  5518  isosolem  5566  oprabid  5640  caovimo  5797  elovmpt2  5804  dfxp3  5923  nnaord  6222  prmuloc  7072  ltrelxr  7494  rexuz2  9004  ltxr  9181  elixx3g  9254  elioo4g  9287  elioopnf  9320  elioomnf  9321  elicopnf  9322  elxrge0  9331  divelunit  9354  elfz2  9366  elfzuzb  9369  uzsplit  9439  fznn0  9460  elfzmlbp  9474  elfzo2  9492  fzolb2  9496  fzouzsplit  9521  ssfzo12bi  9567  fzind2  9581  abs2dif  10438  sumeq2  10643  divalgb  10831  divgcdz  10869  rplpwr  10922  cncongr1  10991  bd3an  11190
  Copyright terms: Public domain W3C validator