Theorem simplr1 1047

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 1011	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantr 466	1 |- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  soltmin  5193  frfi  7764  wemappo  8012  iccsplit  11711  ccatswrd  12753  sqrmo  13254  pcdvdstr  14763  vdwlem12  14880  mreexexlem4d  15491  iscatd2  15525  oppccomfpropd  15570  resssetc  15925  resscatc  15938  mod1ile  16289  mod2ile  16290  prdsmndd  16507  grprcan  16637  prdsringd  17778  lmodprop2d  18088  lssintcl  18125  prdslmodd  18130  islmhm2  18199  islbs3  18316  ofco2  19413  mdetmul  19585  restopnb  20128  regsep2  20329  iuncon  20380  blsscls2  21456  met2ndci  21474  xrsblre  21766  legso  24581  colline  24631  tglowdim2ln  24633  cgrahl  24805  f1otrg  24838  f1otrge  24839  ax5seglem4  24899  ax5seglem5  24900  axcontlem4  24934  axcontlem8  24938  axcontlem9  24939  axcontlem10  24940  eengtrkg  24952  el2wlksotot  25547  rusgranumwlks  25621  extwwlkfablem1  25739  submomnd  28419  ogrpaddltbi  28428  erdszelem8  29868  btwncomim  30724  btwnswapid  30728  broutsideof3  30837  outsideoftr  30840  outsidele  30843  isbasisrelowllem1  31665  isbasisrelowllem2  31666  cvrletrN  32751  ltltncvr  32900  atcvrj2b  32909  2at0mat0  33002  paddasslem11  33307  pmod1i  33325  lautcvr  33569  tendoplass  34262  tendodi1  34263  tendodi2  34264  cdlemk34  34389  mendassa  35973  3adantlr3  37278  ioondisj2  37481  ioondisj1  37482  subsubelfzo0  38859  ply1mulgsumlem2  39772  lincresunit3lem2  39866