Theorem anass 439

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 484  an23 485  an4 506  prlem2 771  3anass 779  4exdistr 1313  2sb5 1335  2sb5rf 1338  sbel2x 1345  euan 1428  r2ex 1691  r19.41v 1763  reeanv 1778  ceqsex2 1836  gencbvex 1838  ceqsrex2v 1890  inass 2223  difrab 2273  axsep2 2704  eqvinop 2791  copsexg 2792  opabid 2810  uniuni 2880  reuxfr2 2903  wefrc 2943  onminex 3020  elxp2 3203  resopab2 3398  asymref 3439  elxp4 3453  elxp5 3454  ssrnres 3481  cores 3499  coass 3512  imadif 3574  fcoi1 3645  imaiun 3864  isoini 3900  f1oiso 3904  dfrdg2 3933  dfoprab2 3991  fnoprval 4017  oprabex3 4022  oprabval3 4030  dfoprab5 4115  foprab2 4119  mapsnen 4429  xpsnen 4435  xpassen 4441  abfii2OLD 4562  zfregs 4647  bnd2 4724  aceq1 4729  aceq5lem1 4735  aceq5lem2 4736  aceq5lem5 4739  kmlem3 4767  kmlem14 4778  ltexpi 5029  genpass 5112  distrlem1pr 5127  distrlem5pr 5131  ltexprlem4 5145  reclem2pr 5157  elreal 5250  axaddopr 5265  axmulopr 5266  infm3 6054  infmsup 6068  zmin 6219  qbtwnre 6278  elioo3g 6380  rexuz 6444  rexuz2 6445  nnwos 6460  elfz2t 6472  elfzlem 6473  sumex 6981  elcncf1d 7270  abscncflem 7274  infpn2 7509  infmap2lem1 7579  istps2 7607  istps3 7608  tgss3t 7638  cncnplem4 7777  blfval2 7836  blrn2 7842  opnin 7869  cncfmet 7905  bcthlem14 8012  grpidinvlem3 8050  pilem1 8671  h2hlm 8850  sh2 9091  ocsh 9156  osumlem5 9582  nmcopexlem1 9951  nmcfnexlem1 9980  cvbr2t 10210  cvnbtwn2t 10214  mdsl2 10249  cvmd 10251  mdsymlem2 10331  sumdmdi 10342  hmeogrp 10538

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