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

Definition df-3an 922
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 920 . 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  924  3anrot  925  3ancoma  927  3anan32  931  3ioran  935  3simpa  936  3pm3.2i  1117  pm3.2an3  1118  3jca  1119  3anbi123i  1128  3imp  1133  3anbi123d  1244  3anim123d  1251  an6  1253  19.26-3an  1413  hb3an  1483  nf3an  1499  nf3and  1502  eeeanv  1851  sb3an  1875  mopick2  2026  r19.26-3  2492  3reeanv  2529  ceqsex3v  2650  ceqsex4v  2651  ceqsex8v  2653  sbc3an  2884  elin3  3173  raltpg  3463  tpss  3570  dfopg  3588  opeq1  3590  opeq2  3591  opm  4017  otth2  4024  poirr  4090  po3nr  4093  wepo  4142  wetrep  4143  rabxp  4426  brinxp2  4453  brinxp  4454  sotri2  4772  sotri3  4773  f1orn  5187  dff1o6  5467  isosolem  5514  oprabid  5588  caovimo  5745  elovmpt2  5752  dfxp3  5871  nnaord  6169  prmuloc  6870  ltrelxr  7292  rexuz2  8802  ltxr  8979  elixx3g  9052  elioo4g  9085  elioopnf  9118  elioomnf  9119  elicopnf  9120  elxrge0  9129  divelunit  9152  elfz2  9164  elfzuzb  9167  uzsplit  9237  fznn0  9258  elfzmlbp  9272  elfzo2  9289  fzolb2  9292  fzouzsplit  9317  ssfzo12bi  9363  fzind2  9377  abs2dif  10193  sumeq2d  10397  sumeq2  10398  divalgb  10532  divgcdz  10570  rplpwr  10623  cncongr1  10692  bd3an  10888
  Copyright terms: Public domain W3C validator