Theorem anass 487

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 374	. . . 4 |- (((ph /\ ps) -> -. ch) <-> (ph -> (ps -> -. ch)))
2		imnan 261	. . . . 5 |- ((ps -> -. ch) <-> -. (ps /\ ch))
3	2	imbi2i 202	. . . 4 |- ((ph -> (ps -> -. ch)) <-> (ph -> -. (ps /\ ch)))
4	1, 3	bitri 190	. . 3 |- (((ph /\ ps) -> -. ch) <-> (ph -> -. (ps /\ ch)))
5	4	notbii 204	. 2 |- (-. ((ph /\ ps) -> -. ch) <-> -. (ph -> -. (ps /\ ch)))
6		df-an 242	. 2 |- (((ph /\ ps) /\ ch) <-> -. ((ph /\ ps) -> -. ch))
7		df-an 242	. 2 |- ((ph /\ (ps /\ ch)) <-> -. (ph -> -. (ps /\ ch)))
8	5, 6, 7	3bitr4i 200	1 |- (((ph /\ ps) /\ ch) <-> (ph /\ (ps /\ ch)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  an12 542  an23 543  an4 564  prlem2OLD 851  3anass 862  4exdistr 1695  2sb5 1725  2sb5rf 1728  sbel2x 1736  euanOLD 1828  r2ex 2152  r19.41 2235  reeanOLD 2248  ceqsex2OLD 2327  ceqsex3v 2330  gencbvexOLD 2335  ceqsrex2v 2395  inass 2804  difrab 2868  inssdif0 2940  axsep2 3439  eqvinop 3536  copsexg 3537  copsexgOLD 3538  opabidOLD 3558  wefrc 3652  uniuni 3806  eufromeq4 3831  reuxfr2d 3844  reuxfr2 3845  onminex 3888  elxp2 4019  elvvv 4054  resopab2 4256  asymrefOLD 4309  ssrnres 4354  elxp4 4379  elxp5 4380  coresOLD 4401  coass 4415  imadif 4493  fcoi1OLD 4585  dff1o2 4639  eqfnfv3 4769  imaiun 4840  isoini 4877  f1oiso 4881  dfoprab2 4917  fnoprv 4946  oprabex3 4951  oprabval3 4959  foprab2 5061  dfrdg2 5141  mapsnen 5488  xpsnen 5494  xpassen 5500  abfii2 5652  zfregs 5754  bnd2 5854  aceq1 5891  aceq5lem1 5897  aceq5lem2 5898  aceq5lem5 5901  kmlem3 5929  kmlem14 5940  ltexpi 6181  genpass 6264  distrlem1pr 6279  distrlem5pr 6283  ltexprlem4 6297  reclem2pr 6309  elreal 6402  axaddopr 6417  axmulopr 6418  infm3 7263  infmsup 7277  zmin 7432  qbtwnre 7459  elioo3g 7547  rexuz 7613  rexuz2 7614  nnwos 7629  elfz2 7642  elfzlem 7643  fzsuc 7678  sumex 8241  elcncf1di 8532  abscncflem 8536  infpn2 8778  infmap2lem1 8848  istps2 8876  istps3 8877  tgss3 8908  cncnplem4 9054  blfval2 9113  blrn2 9119  opnin 9146  cncfmet 9183  bcthlem14 9290  grpidinvlem3 9330  pilem1 10020  filmapf 10307  h2hlm 10482  sh2 10724  ocsh 10789  osumlem5 11217  nmcopexlem1 11588  nmcfnexlem1 11617  cvbr2 11855  cvnbtwn2 11859  mdsl2i 11894  cvmdi 11896  mdsymlem2 11976  sumdmdii 11987  bnj170OLD 12035  bnj172OLD 12039  bnj173OLD 12041  bnj174OLD 12043  bnj176OLD 12046  bnj250 12089  bnj251 12090  bnj256 12095  bnj50OLD 12425  bnj142 12474  bnj162OLD 12488  bnj168 12496  bnj849 13318  divalglem10 13705  divalgb 13707  isprm2 13775  axacprim 13791  indifdi 13823  wfi 13915  frind 13939  frxp 13951  sltval2 13997  dfon3 14072  fnoprvpop 14338  dfoprab4spop 14339  prodex 14656  hmeogrp 14892  cnvresima 15359  compfipin0 15436  is1stc3 15469  topmeet 15526  neifg 15559  rexrab 15671  difin2 15676  resoprab2 15710  eqfnfv3OLD 15721  frminex 15773  fzsplit 15792  sdc 15811  txmet 15925  isbnd3 15941  heiborlem1 15955  heiborlem24 15978  phtpyfval 16046  phtpyval 16047  phtpcval 16058  pi1bvalqs 16091  prtlem70 16238  prtlem100 16244  prtlem16 16272  prtlem18 16279  prter3 16286  strdif 16719  cvrval2 16991  cvrnbtwn2 16992  grpidinvlem3NEW 17111  pmapjat 17314

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 164  df-an 242

Copyright terms: Public domain