Theorem anasss 442

Description: Associative law for conjunction applied to antecedent (eliminates syllogism).

Hypothesis

Ref	Expression
anasss.1	|- (((ph /\ ps) /\ ch) -> th)

Assertion

Ref	Expression
anasss	|- ((ph /\ (ps /\ ch)) -> th)

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 378	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 363	1 |- ((ph /\ (ps /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  tz6.12-1 3742  oecl 4178  oaass 4201  oen0 4219  oeordi 4220  oeworde 4226  mapxpen 4501  fodomfi 4575  fodomfiOLD 4576  supmo 4585  cardinfima 4902  distrlem4pr 5142  xrlttrt 5565  ltmul12it 5843  uzindOLD 6210  uzind3OLD 6211  uzwo4OLD 6212  qrecclt 6274  eluzp1m1t 6434  expord2t 6605  fsumsplit 7020  fsumcom 7028  fsumrev 7029  fsumdivc 7035  fsumdivcALT 7036  fsumcmpndx2 7042  climge0 7112  climaddlem3 7116  climmullem4 7123  climmullem5 7124  climmullem8 7127  clim2serzt 7134  cvgratlem1 7250  mulc1cncf 7279  tgtopt 7627  neissex 7735  bl2in 7840  blss 7850  blssex 7851  metcnss2 7896  lmnn 7932  lmfexlem3 7955  lmle 7957  xpcn 7973  bcthlem24 8019  bcthlem25 8020  bcthlem26 8021  grpidinvlem4 8048  ghgrpilem4 8132  ghgrpi 8133  0lno 8446  htthlem10 8625  shmods 9357  eighmortht 9883  nmcopexlem5 9950  nmcopexlem6 9951  nmcfnexlem5 9979  nmcfnexlem6 9980  kbass5t 10048  kbass6t 10049  hmopidmch 10074  hstel2t 10141  dmdmdt 10222  atom1d 10275  superpos 10276  atcvat4 10319  mdsymlem2 10326  mdsymlem3 10327  mdsymlem4 10328  mdsymlem5 10329

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