Theorem anassrs 397

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 362	. 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  398  mpanr1  433  anass1rs  560  anabss5  567  anabss7  572  2ralbida  2456  2rexbidva  2458  ralimdvva  2501  pofun  4234  issod  4241  imainss  4954  fvelimab  5477  eqfnfv2  5519  funconstss  5538  fnex  5642  rexima  5656  ralima  5657  f1elima  5674  fliftfun  5697  isores2  5714  isosolem  5725  f1oiso  5727  ovmpodxf  5896  grpridd  5967  tfrlemibxssdm  6224  oav2  6359  omv2  6361  nnaass  6381  eroveu  6520  prarloclem4  7306  genpml  7325  genpmu  7326  genpassl  7332  genpassu  7333  prmuloc2  7375  addcomprg  7386  mulcomprg  7388  ltaddpr  7405  ltexprlemloc  7415  addcanprlemu  7423  recexgt0sr  7581  reapmul1  8357  apreim  8365  recexaplem2  8413  creur  8717  uz11  9348  xaddass  9652  xleadd1a  9656  xlt2add  9663  fzrevral  9885  seq3caopr2  10255  expnlbnd2  10417  shftlem  10588  resqrexlemgt0  10792  cau3lem  10886  clim2  11052  clim2c  11053  clim0c  11055  2clim  11070  climabs0  11076  climcn1  11077  climcn2  11078  climsqz  11104  climsqz2  11105  summodclem2  11151  fsum2dlemstep  11203  fsumiun  11246  mertenslem2  11305  mertensabs  11306  prodfrecap  11315  gcdmultiplez  11709  dvdssq  11719  lcmgcdlem  11758  lcmdvds  11760  coprmdvds2  11774  neipsm  12323  lmbrf  12384  lmss  12415  txbas  12427  txbasval  12436  tx1cn  12438  txlm  12448  isxmet2d  12517  elmopn2  12618  mopni3  12653  blsscls2  12662  metequiv2  12665  metss2lem  12666  metrest  12675  metcnp  12681  metcnp2  12682  metcnpi3  12686  elcncf2  12730  mulc1cncf  12745  cncfco  12747  cncfmet  12748