Theorem anassrs 393

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

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

Assertion

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

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 358	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 253	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  anass  394  mpanr1  429  anass1rs  539  anabss5  546  anabss7  551  2ralbida  2400  2rexbidva  2402  pofun  4148  issod  4155  imainss  4860  fvelimab  5373  eqfnfv2  5412  funconstss  5431  fnex  5533  rexima  5548  ralima  5549  f1elima  5566  fliftfun  5589  isores2  5606  isosolem  5617  f1oiso  5619  ovmpt2dxf  5784  grpridd  5855  tfrlemibxssdm  6106  oav2  6238  omv2  6240  nnaass  6260  eroveu  6397  prarloclem4  7118  genpml  7137  genpmu  7138  genpassl  7144  genpassu  7145  prmuloc2  7187  addcomprg  7198  mulcomprg  7200  ltaddpr  7217  ltexprlemloc  7227  addcanprlemu  7235  recexgt0sr  7380  reapmul1  8133  apreim  8141  recexaplem2  8182  creur  8480  uz11  9102  fzrevral  9580  iseqcaopr2  9972  expnlbnd2  10140  shftlem  10311  resqrexlemgt0  10514  cau3lem  10608  clim2  10732  clim2c  10733  clim0c  10735  2clim  10750  climabs0  10757  climcn1  10758  climcn2  10759  climsqz  10784  climsqz2  10785  isummolem2  10833  fsum2dlemstep  10889  fsumiun  10932  mertenslem2  10991  mertensabs  10992  gcdmultiplez  11349  dvdssq  11359  lcmgcdlem  11398  lcmdvds  11400  coprmdvds2  11414  elcncf2  11903  mulc1cncf  11918  cncfco  11920