Theorem anass 336

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 276	. . . 4 |- (((ph /\ ps) -> -. ch) <-> (ph -> (ps -> -. ch)))
2		imnan 207	. . . . 5 |- ((ps -> -. ch) <-> -. (ps /\ ch))
3	2	imbi2i 160	. . . 4 |- ((ph -> (ps -> -. ch)) <-> (ph -> -. (ps /\ ch)))
4	1, 3	bitr 151	. . 3 |- (((ph /\ ps) -> -. ch) <-> (ph -> -. (ps /\ ch)))
5	4	negbii 162	. 2 |- (-. ((ph /\ ps) -> -. ch) <-> -. (ph -> -. (ps /\ ch)))
6		df-an 198	. 2 |- (((ph /\ ps) /\ ch) <-> -. ((ph /\ ps) -> -. ch))
7		df-an 198	. 2 |- ((ph /\ (ps /\ ch)) <-> -. (ph -> -. (ps /\ ch)))
8	5, 6, 7	3bitr4 158	1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  an12 370  an23 371  an4 388  biass 511  prlem2 577  3anass 585  4exdistr 971  sbel2x 995  euanv 1053  r2ex 1241  r19.41v 1302  reeanv 1316  gencbvex 1372  reuxfr2 1579  inass 1650  difrab 1695  eqvinop 1901  copsexg 1902  opabid 2099  wefrc 2195  onminex 2275  elxp2 2443  cbvop 2473  elxp4 2640  elxp5 2641  imaiun 2650  cores 2659  coass 2667  imadif 2714  fcoi1 2765  isoini 2938  f1oiso 2942  dfoprab2 3021  fnoprval 3042  oprabex3 3046  oprabval3 3052  mapsnen 3334  xpsnen 3339  xpassen 3344  zfregs 3491  bnd2 3549  aceq1 3552  aceq5lem1 3558  aceq5lem2 3559  aceq5lem5 3562  kmlem3 3582  kmlem14 3593  ltexpi 3823  genpass 3906  distrlem1pr 3921  distrlem5pr 3925  ltexprlem4 3939  reclem2pr 3951  elreal 4044  nnwos 4610  zmin 4617  qbtwnre 4650  infmap2lem1 4951  sh2 5126  ocsh 5164  osumlem5 5534  cvbr2t 5715  cvnbtwn2t 5719  mdsymlem2 5777  sumdmdi 5785

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org