Theorem anass 450

Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118.

Assertion

Ref	Expression
anass	|- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		impexp 354	. . . 4 |- (((ph /\ ps) -> -. ch) <-> (ph -> (ps -> -. ch)))
2		imnan 249	. . . . 5 |- ((ps -> -. ch) <-> -. (ps /\ ch))
3	2	imbi2i 192	. . . 4 |- ((ph -> (ps -> -. ch)) <-> (ph -> -. (ps /\ ch)))
4	1, 3	bitri 180	. . 3 |- (((ph /\ ps) -> -. ch) <-> (ph -> -. (ps /\ ch)))
5	4	notbii 194	. 2 |- (-. ((ph /\ ps) -> -. ch) <-> -. (ph -> -. (ps /\ ch)))
6		df-an 232	. 2 |- (((ph /\ ps) /\ ch) <-> -. ((ph /\ ps) -> -. ch))
7		df-an 232	. 2 |- ((ph /\ (ps /\ ch)) <-> -. (ph -> -. (ps /\ ch)))
8	5, 6, 7	3bitr4i 190	1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 153   /\ wa 230

This theorem is referenced by:  an12 495  an23 496  an4 517  prlem2 783  3anass 791  4exdistr 1355  2sb5 1377  2sb5rf 1380  sbel2x 1387  euan 1470  r2ex 1738  r19.41v 1810  reeanv 1825  ceqsex2 1883  gencbvex 1885  ceqsrex2v 1937  inass 2274  difrab 2324  axsep2 2759  eqvinop 2847  copsexg 2848  opabid 2866  uniuni 2937  reuxfr2 2960  wefrc 3000  onminex 3077  elxp2 3260  resopab2 3455  asymref 3496  elxp4 3510  elxp5 3511  ssrnres 3538  cores 3556  coass 3569  imadif 3631  fcoi1 3702  imaiun 3921  isoini 3958  f1oiso 3962  dfrdg2 3991  dfoprab2 4049  fnoprval 4075  oprabex3 4080  oprabval3 4088  dfoprab5 4173  foprab2 4177  mapsnen 4490  xpsnen 4498  xpassen 4504  abfii2 4622  zfregs 4709  bnd2 4786  aceq1 4791  aceq5lem1 4797  aceq5lem2 4798  aceq5lem5 4801  kmlem3 4829  kmlem14 4840  ltexpi 5094  genpass 5177  distrlem1pr 5192  distrlem5pr 5196  ltexprlem4 5210  reclem2pr 5222  elreal 5315  axaddopr 5330  axmulopr 5331  infm3 6136  infmsup 6150  zmin 6304  qbtwnre 6331  elioo3g 6405  rexuz 6470  rexuz2 6471  nnwos 6486  elfz2 6498  elfzlem 6499  sumex 7071  elcncf1di 7360  abscncflem 7364  infpn2 7601  infmap2lem1 7671  istps2 7698  istps3 7699  tgss3 7727  cncnplem4 7862  blfval2 7921  blrn2 7927  opnin 7954  cncfmet 7990  bcthlem14 8097  grpidinvlem3 8135  pilem1 8754  h2hlm 8933  sh2 9174  ocsh 9239  osumlem5 9665  nmcopexlem1 10034  nmcfnexlem1 10063  cvbr2 10294  cvnbtwn2 10298  mdsl2i 10333  cvmdi 10335  mdsymlem2 10415  sumdmdii 10426  hmeogrp 10632

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain