HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 impexp 347 . . . 4 |- (((ph /\ ps) -> -. ch) <-> (ph -> (ps -> -. ch)))
2 imnan 242 . . . . 5 |- ((ps -> -. ch) <-> -. (ps /\ ch))
32imbi2i 185 . . . 4 |- ((ph -> (ps -> -. ch)) <-> (ph -> -. (ps /\ ch)))
41, 3bitr 173 . . 3 |- (((ph /\ ps) -> -. ch) <-> (ph -> -. (ps /\ ch)))
54negbii 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)))
85, 6, 73bitr4 183 1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223
This theorem is referenced by:  an12 484  an23 485  an4 506  prlem2 770  3anass 778  4exdistr 1311  2sb5 1333  2sb5rf 1336  sbel2x 1343  euan 1426  r2ex 1688  r19.41v 1760  reeanv 1775  ceqsex2 1832  gencbvex 1834  ceqsrex2v 1886  inass 2219  difrab 2269  axsep2 2699  eqvinop 2786  copsexg 2787  opabid 2805  uniuni 2875  reuxfr2 2898  wefrc 2938  onminex 3015  elxp2 3198  resopab2 3390  asymref 3431  elxp4 3445  elxp5 3446  ssrnres 3473  cores 3491  coass 3504  imadif 3566  fcoi1 3636  imaiun 3855  isoini 3891  f1oiso 3895  dfrdg2 3924  dfoprab2 3982  fnoprval 4008  oprabex3 4013  oprabval3 4021  dfoprab5 4105  foprab2 4109  mapsnen 4416  xpsnen 4421  xpassen 4427  abfii2 4542  zfregs 4627  bnd2 4704  aceq1 4709  aceq5lem1 4715  aceq5lem2 4716  aceq5lem5 4719  kmlem3 4747  kmlem14 4758  ltexpi 5009  genpass 5092  distrlem1pr 5107  distrlem5pr 5111  ltexprlem4 5125  reclem2pr 5137  elreal 5230  axaddopr 5245  axmulopr 5246  infm3 6009  infmsup 6023  zmin 6175  qbtwnre 6224  elioo3g 6325  rexuz 6384  rexuz2 6385  nnwos 6400  elfz2t 6412  elfzlem 6413  sumex 6927  elcncf1d 7213  abscncflem 7217  infpn2 7460  infmap2lem1 7529  istps2 7557  istps3 7558  tgss3t 7588  cncnplem4 7727  blfval2 7788  blrn2 7794  opnin 7821  cncfmet 7857  bcthlem14 7962  grpidinvlem3 8000  pilem1 8609  h2hlm 8789  sh2 9030  ocsh 9095  osumlem5 9522  nmcopexlem1 9889  nmcfnexlem1 9918  cvbr2t 10148  cvnbtwn2t 10152  mdsl2 10186  cvmd 10188  mdsymlem2 10268  sumdmdi 10278  hmeogrp 10461
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