Theorem anasss 451

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 385	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 370	1 |- ((ph /\ (ps /\ ch)) -> th)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  tz6.12-1 3793  oecl 4230  oaass 4253  oen0 4271  oeordi 4272  oeworde 4278  mapxpen 4560  fodomfi 4626  supmo 4636  cardinfima 4956  distrlem4pr 5195  xrlttr 5618  ltmul12a 5899  uzindOLD 6293  uzind3OLD 6294  uzwo4OLD 6295  qreccl 6325  quoremnn0ALT 6364  eluzp1m1 6459  expord2 6693  fsumspl 7110  fsumcom 7118  fsumrev 7119  fsumdivc 7125  fsumdivcALT 7126  fsumcmpndx2 7132  climge0 7202  climaddlem3 7206  climmullem4 7213  climmullem5 7214  climmullem8 7217  clim2serz 7224  cvgratlem1 7340  mulc1cncf 7369  tgtop 7717  neissex 7823  bl2in 7928  blss 7938  blssex 7939  metcnss2 7984  lmnn 8020  lmfexlem3 8043  lmle 8045  xpcn 8061  bcthlem24 8107  bcthlem25 8108  bcthlem26 8109  grpidinvlem4 8136  ghgrpilem4 8220  ghgrpi 8221  0lno 8534  htthlem10 8713  shmodsi 9445  eighmorth 9971  nmcopexlem5 10038  nmcopexlem6 10039  nmcfnexlem5 10067  nmcfnexlem6 10068  kbass5 10136  kbass6 10137  hmopidmchi 10162  hstel2 10230  dmdmd 10311  atom1d 10364  superpos 10365  atcvat4i 10408  mdsymlem2 10415  mdsymlem3 10416  mdsymlem4 10417  mdsymlem5 10418

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 154  df-an 232

Copyright terms: Public domain