Theorem anassrs 398

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 363	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 254	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  anass  399  mpanr1  434  anass1rs  561  anabss5  568  anabss7  573  2ralbida  2459  2rexbidva  2461  ralimdvva  2504  pofun  4242  issod  4249  imainss  4962  fvelimab  5485  eqfnfv2  5527  funconstss  5546  fnex  5650  rexima  5664  ralima  5665  f1elima  5682  fliftfun  5705  isores2  5722  isosolem  5733  f1oiso  5735  ovmpodxf  5904  grpridd  5975  tfrlemibxssdm  6232  oav2  6367  omv2  6369  nnaass  6389  eroveu  6528  prarloclem4  7330  genpml  7349  genpmu  7350  genpassl  7356  genpassu  7357  prmuloc2  7399  addcomprg  7410  mulcomprg  7412  ltaddpr  7429  ltexprlemloc  7439  addcanprlemu  7447  recexgt0sr  7605  reapmul1  8381  apreim  8389  recexaplem2  8437  creur  8741  uz11  9372  xaddass  9682  xleadd1a  9686  xlt2add  9693  fzrevral  9916  seq3caopr2  10286  expnlbnd2  10448  shftlem  10620  resqrexlemgt0  10824  cau3lem  10918  clim2  11084  clim2c  11085  clim0c  11087  2clim  11102  climabs0  11108  climcn1  11109  climcn2  11110  climsqz  11136  climsqz2  11137  summodclem2  11183  fsum2dlemstep  11235  fsumiun  11278  mertenslem2  11337  mertensabs  11338  prodfrecap  11347  gcdmultiplez  11745  dvdssq  11755  lcmgcdlem  11794  lcmdvds  11796  coprmdvds2  11810  neipsm  12362  lmbrf  12423  lmss  12454  txbas  12466  txbasval  12475  tx1cn  12477  txlm  12487  isxmet2d  12556  elmopn2  12657  mopni3  12692  blsscls2  12701  metequiv2  12704  metss2lem  12705  metrest  12714  metcnp  12720  metcnp2  12721  metcnpi3  12725  elcncf2  12769  mulc1cncf  12784  cncfco  12786  cncfmet  12787