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

Definition df-3an 898
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 387. (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 896 . 2  wff  ( ph  /\ 
ps  /\  ch )
51, 2wa 101 . . 3  wff  ( ph  /\ 
ps )
65, 3wa 101 . 2  wff  ( (
ph  /\  ps )  /\  ch )
74, 6wb 102 1  wff  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
Colors of variables: wff set class
This definition is referenced by:  3anass  900  3anrot  901  3ancoma  903  3anan32  907  3ioran  911  3simpa  912  3pm3.2i  1093  pm3.2an3  1094  3jca  1095  3anbi123i  1104  3imp  1109  3anbi123d  1218  3anim123d  1225  an6  1227  19.26-3an  1388  hb3an  1458  nf3an  1474  nf3and  1477  eeeanv  1824  sb3an  1848  mopick2  1999  r19.26-3  2460  3reeanv  2497  ceqsex3v  2613  ceqsex4v  2614  ceqsex8v  2616  sbc3an  2846  elin3  3155  raltpg  3450  tpss  3556  dfopg  3574  opeq1  3576  opeq2  3577  opm  3998  otth2  4005  poirr  4071  po3nr  4074  wepo  4123  wetrep  4124  rabxp  4407  brinxp2  4434  brinxp  4435  sotri2  4749  sotri3  4750  f1orn  5163  dff1o6  5443  isosolem  5490  oprabid  5564  caovimo  5721  elovmpt2  5728  dfxp3  5847  nnaord  6112  prmuloc  6721  ltrelxr  7138  rexuz2  8619  ltxr  8795  elixx3g  8870  elioo4g  8903  elioopnf  8936  elioomnf  8937  elicopnf  8938  elxrge0  8947  divelunit  8970  elfz2  8982  elfzuzb  8985  uzsplit  9055  fznn0  9075  elfzmlbp  9091  elfzo2  9108  fzolb2  9111  fzouzsplit  9136  ssfzo12bi  9182  fzind2  9196  abs2dif  9932  bd3an  10316
  Copyright terms: Public domain W3C validator