Theorem anasss 647

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

Hypothesis

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

Assertion

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

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 604	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 433	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  anass  649  anabss3  821  f1elima  6157  fnfvof  6535  oecl  7184  oaass  7207  oen0  7232  oeworde  7239  omabs  7293  oiiniseg  7954  cardinfima  8474  fpwwe2lem12  9015  ltmul12a  10394  uzindOLD  10951  uzind3OLD  10952  eluzp1m1  11101  lbzbi  11166  qreccl  11198  xrlttr  11342  elfzodifsumelfzo  11846  quoremnn0  11947  incexc2  13609  mertens  13654  ndvdsadd  13921  nn0seqcvgd  14054  isprm3  14081  pcval  14223  prdsval  14706  evlfcl  15345  frgpup1  16589  frgpup3lem  16591  gsumval3OLD  16699  gsumval3  16702  gsumzoppg  16758  gsumzoppgOLD  16759  ablfaclem2  16927  gsumdixpOLD  17041  gsumdixp  17042  psrass1lem  17800  psrass1  17831  frlmgsumOLD  18568  frlmgsum  18569  m2cpminvid2  19023  pmatcollpw2lem  19045  chcoeffeqlem  19153  neissex  19394  neiptopnei  19399  tx1stc  19886  kqreglem1  19977  xpstopnlem1  20045  alexsublem  20279  psmettri2  20548  metuel2  20817  icoopnst  21174  iocopnst  21175  volcn  21750  mbflimsup  21808  mbflim  21810  itg1addlem4  21841  itg1addlem5  21842  itg1climres  21856  limcflf  22020  dvcobr  22084  dvcnvlem  22112  dvfsumge  22158  mdegmullem  22213  plyeq0lem  22342  plypf1  22344  mtestbdd  22534  mbfulm  22535  fsumdvdscom  23189  muinv  23197  logfaclbnd  23225  logexprlim  23228  dchrinv  23264  lgsval3  23317  rpvmasum2  23425  dchrisum0lem1  23429  dchrisum0  23433  selberg  23461  selberg3lem1  23470  selberg34r  23484  pntsval2  23489  ercgrg  23636  legso  23712  colinearalg  23889  axeuclid  23942  axcontlem2  23944  axcontlem7  23949  grpoidinvlem4  24885  ipblnfi  25447  shmodsi  25983  eighmorth  26559  kbass5  26715  kbass6  26716  dmdmd  26895  atom1d  26948  mdsymlem2  26999  mdsymlem3  27000  mdsymlem4  27001  mdsymlem5  27002  ofrn  27152  gsummpt2co  27434  suborng  27468  pstmxmet  27512  ordtconlem1  27542  dya2iocnei  27893  rescon  28331  nocvxminlem  29027  nobndlem6  29034  fin2so  29617  ismblfin  29632  mbfposadd  29639  itg2gt0cn  29647  ftc1anclem7  29673  ftc1anc  29675  cover2  29807  indexa  29827  filbcmb  29834  seqpo  29843  incsequz  29844  isbnd2  29882  ghomco  29948  unichnidl  30031  isfldidl  30068  isprm7  30795  dihvalc  36030  dihvalb  36034