Theorem anasss 440

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 376	. 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 3721  oecl 4156  oaass 4179  oen0 4197  oeordi 4198  oeworde 4204  mapxpen 4475  fodomfi 4540  supmo 4550  cardinfima 4863  distrlem4pr 5102  xrlttrt 5526  ltmul12it 5797  uzindOLD 6156  uzind3OLD 6157  uzwo4OLD 6158  qrecclt 6211  eluzp1m1t 6365  expord2t 6535  fsumsplit 6958  fsumcom 6966  fsumrev 6967  fsumdivc 6973  fsumdivcALT 6974  fsumcmpndx2 6980  climge0 7049  climaddlem3 7052  climmullem4 7059  climmullem5 7060  climmullem8 7063  clim2serzt 7070  cvgratlem1 7185  mulc1cncf 7214  tgtopt 7570  neissex 7679  bl2in 7783  blss 7793  blssex 7794  metcnss2 7838  lmnn 7873  lmfexlem3 7893  lmle 7895  xpcn 7910  bcthlem24 7956  bcthlem25 7957  bcthlem26 7958  grpidinvlem4 7985  ghgrpilem4 8073  ghgrpi 8074  0lno 8382  htthlem10 8559  shmods 9277  eighmortht 9804  nmcopexlem5 9870  nmcopexlem6 9871  nmcfnexlem5 9899  nmcfnexlem6 9900  kbass5t 9965  kbass6t 9966  hmopidmch 9990  hstel2t 10056  dmdmdt 10137  atom1d 10188  superpos 10189  atcvat4 10232  mdsymlem2 10239  mdsymlem3 10240  mdsymlem4 10241  mdsymlem5 10242

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