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  435  anass1rs  566  anabss5  573  anabss7  578  2ralbida  2491  2rexbidva  2493  ralimdvva  2539  pofun  4297  issod  4304  imainss  5026  fvelimab  5552  eqfnfv2  5594  funconstss  5614  fnex  5718  rexima  5734  ralima  5735  f1elima  5752  fliftfun  5775  isores2  5792  isosolem  5803  f1oiso  5805  ovmpodxf  5978  tfrlemibxssdm  6306  oav2  6442  omv2  6444  nnaass  6464  eroveu  6604  prarloclem4  7460  genpml  7479  genpmu  7480  genpassl  7486  genpassu  7487  prmuloc2  7529  addcomprg  7540  mulcomprg  7542  ltaddpr  7559  ltexprlemloc  7569  addcanprlemu  7577  recexgt0sr  7735  reapmul1  8514  apreim  8522  recexaplem2  8570  creur  8875  uz11  9509  xaddass  9826  xleadd1a  9830  xlt2add  9837  fzrevral  10061  seq3caopr2  10438  expnlbnd2  10601  shftlem  10780  resqrexlemgt0  10984  cau3lem  11078  clim2  11246  clim2c  11247  clim0c  11249  2clim  11264  climabs0  11270  climcn1  11271  climcn2  11272  climsqz  11298  climsqz2  11299  summodclem2  11345  fsum2dlemstep  11397  fsumiun  11440  mertenslem2  11499  mertensabs  11500  prodfrecap  11509  fprodeq0  11580  fprod2dlemstep  11585  gcdmultiplez  11976  dvdssq  11986  lcmgcdlem  12031  lcmdvds  12033  coprmdvds2  12047  pclemub  12241  pcge0  12266  pcgcd1  12281  prmpwdvds  12307  1arithlem4  12318  grpidpropdg  12628  grpridd  12641  mhmpropd  12689  mhmima  12706  grplcan  12761  neipsm  12948  lmbrf  13009  lmss  13040  txbas  13052  txbasval  13061  tx1cn  13063  txlm  13073  isxmet2d  13142  elmopn2  13243  mopni3  13278  blsscls2  13287  metequiv2  13290  metss2lem  13291  metrest  13300  metcnp  13306  metcnp2  13307  metcnpi3  13311  elcncf2  13355  mulc1cncf  13370  cncfco  13372  cncfmet  13373  2sqlem9  13754