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  2486  2rexbidva  2488  ralimdvva  2534  pofun  4289  issod  4296  imainss  5018  fvelimab  5541  eqfnfv2  5583  funconstss  5602  fnex  5706  rexima  5722  ralima  5723  f1elima  5740  fliftfun  5763  isores2  5780  isosolem  5791  f1oiso  5793  ovmpodxf  5963  grpridd  6034  tfrlemibxssdm  6291  oav2  6427  omv2  6429  nnaass  6449  eroveu  6588  prarloclem4  7435  genpml  7454  genpmu  7455  genpassl  7461  genpassu  7462  prmuloc2  7504  addcomprg  7515  mulcomprg  7517  ltaddpr  7534  ltexprlemloc  7544  addcanprlemu  7552  recexgt0sr  7710  reapmul1  8489  apreim  8497  recexaplem2  8545  creur  8850  uz11  9484  xaddass  9801  xleadd1a  9805  xlt2add  9812  fzrevral  10036  seq3caopr2  10413  expnlbnd2  10576  shftlem  10754  resqrexlemgt0  10958  cau3lem  11052  clim2  11220  clim2c  11221  clim0c  11223  2clim  11238  climabs0  11244  climcn1  11245  climcn2  11246  climsqz  11272  climsqz2  11273  summodclem2  11319  fsum2dlemstep  11371  fsumiun  11414  mertenslem2  11473  mertensabs  11474  prodfrecap  11483  fprodeq0  11554  fprod2dlemstep  11559  gcdmultiplez  11950  dvdssq  11960  lcmgcdlem  12005  lcmdvds  12007  coprmdvds2  12021  pclemub  12215  pcge0  12240  pcgcd1  12255  prmpwdvds  12281  1arithlem4  12292  neipsm  12754  lmbrf  12815  lmss  12846  txbas  12858  txbasval  12867  tx1cn  12869  txlm  12879  isxmet2d  12948  elmopn2  13049  mopni3  13084  blsscls2  13093  metequiv2  13096  metss2lem  13097  metrest  13106  metcnp  13112  metcnp2  13113  metcnpi3  13117  elcncf2  13161  mulc1cncf  13176  cncfco  13178  cncfmet  13179  2sqlem9  13560