Theorem anass 441

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 347	. . . 4 |- (((ph /\ ps) -> -. ch) <-> (ph -> (ps -> -. ch)))
2		imnan 242	. . . . 5 |- ((ps -> -. ch) <-> -. (ps /\ ch))
3	2	imbi2i 185	. . . 4 |- ((ph -> (ps -> -. ch)) <-> (ph -> -. (ps /\ ch)))
4	1, 3	bitr 173	. . 3 |- (((ph /\ ps) -> -. ch) <-> (ph -> -. (ps /\ ch)))
5	4	negbii 187	. 2 |- (-. ((ph /\ ps) -> -. ch) <-> -. (ph -> -. (ps /\ ch)))
6		df-an 225	. 2 |- (((ph /\ ps) /\ ch) <-> -. ((ph /\ ps) -> -. ch))
7		df-an 225	. 2 |- ((ph /\ (ps /\ ch)) <-> -. (ph -> -. (ps /\ ch)))
8	5, 6, 7	3bitr4 183	1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  an12 486  an23 487  an4 508  prlem2 773  3anass 781  4exdistr 1315  2sb5 1337  2sb5rf 1340  sbel2x 1347  euan 1430  r2ex 1694  r19.41v 1766  reeanv 1781  ceqsex2 1839  gencbvex 1841  ceqsrex2v 1893  inass 2226  difrab 2276  axsep2 2709  eqvinop 2797  copsexg 2798  opabid 2816  uniuni 2886  reuxfr2 2909  wefrc 2949  onminex 3026  elxp2 3209  resopab2 3404  asymref 3445  elxp4 3459  elxp5 3460  ssrnres 3487  cores 3505  coass 3518  imadif 3580  fcoi1 3651  imaiun 3870  isoini 3906  f1oiso 3910  dfrdg2 3939  dfoprab2 3997  fnoprval 4023  oprabex3 4028  oprabval3 4036  dfoprab5 4121  foprab2 4125  mapsnen 4435  xpsnen 4441  xpassen 4447  zfregs 4657  bnd2 4734  aceq1 4739  aceq5lem1 4745  aceq5lem2 4746  aceq5lem5 4749  kmlem3 4777  kmlem14 4788  ltexpi 5041  genpass 5124  distrlem1pr 5139  distrlem5pr 5143  ltexprlem4 5157  reclem2pr 5169  elreal 5262  axaddopr 5277  axmulopr 5278  infm3 6056  infmsup 6070  zmin 6221  qbtwnre 6279  elioo3g 6381  rexuz 6445  rexuz2 6446  nnwos 6461  elfz2t 6473  elfzlem 6474  sumex 6981  elcncf1d 7270  abscncflem 7274  infpn2 7510  infmap2lem1 7581  istps2 7608  istps3 7609  tgss3t 7637  cncnplem4 7774  blfval2 7833  blrn2 7839  opnin 7866  cncfmet 7902  bcthlem14 8009  grpidinvlem3 8047  pilem1 8666  h2hlm 8845  sh2 9086  ocsh 9151  osumlem5 9577  nmcopexlem1 9946  nmcfnexlem1 9975  cvbr2t 10205  cvnbtwn2t 10209  mdsl2 10244  cvmd 10246  mdsymlem2 10326  sumdmdi 10337  hmeogrp 10524

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 147  df-an 225

Copyright terms: Public domain