Theorem simplr1 1103

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simplr1

Step	Hyp	Ref	Expression
1		simpr1 1067	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantr 481	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soltmin  5532  frfi  8205  wemappo  8454  iccsplit  12305  ccatswrd  13456  sqrmo  13992  pcdvdstr  15580  vdwlem12  15696  mreexexlem4d  16307  iscatd2  16342  oppccomfpropd  16387  resssetc  16742  resscatc  16755  mod1ile  17105  mod2ile  17106  prdsmndd  17323  grprcan  17455  prdsringd  18612  lmodprop2d  18925  lssintcl  18964  prdslmodd  18969  islmhm2  19038  islbs3  19155  ofco2  20257  mdetmul  20429  restopnb  20979  regsep2  21180  iunconn  21231  blsscls2  22309  met2ndci  22327  xrsblre  22614  legso  25494  colline  25544  tglowdim2ln  25546  cgrahl  25718  f1otrg  25751  f1otrge  25752  ax5seglem4  25812  ax5seglem5  25813  axcontlem4  25847  axcontlem8  25851  axcontlem9  25852  axcontlem10  25853  eengtrkg  25865  rusgrnumwwlks  26869  frgr3v  27139  submomnd  29710  ogrpaddltbi  29719  erdszelem8  31180  nosupbnd1lem5  31858  conway  31910  btwncomim  32120  btwnswapid  32124  broutsideof3  32233  outsideoftr  32236  outsidele  32239  isbasisrelowllem1  33203  isbasisrelowllem2  33204  cvrletrN  34560  ltltncvr  34709  atcvrj2b  34718  2at0mat0  34811  paddasslem11  35116  pmod1i  35134  lautcvr  35378  tendoplass  36071  tendodi1  36072  tendodi2  36073  cdlemk34  36198  mendassa  37764  3adantlr3  39200  ssinc  39264  ssdec  39265  ioondisj2  39714  ioondisj1  39715  subsubelfzo0  41336  ply1mulgsumlem2  42175  lincresunit3lem2  42269