Theorem simplr1 1036

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

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  soltmin  5391  frfi  7757  wemappo  7966  iccsplit  11656  ccatswrd  12672  sqrmo  13167  pcdvdstr  14483  vdwlem12  14594  mreexexlem4d  15136  iscatd2  15170  oppccomfpropd  15215  resssetc  15570  resscatc  15583  mod1ile  15934  mod2ile  15935  prdsmndd  16152  grprcan  16282  prdsringd  17456  lmodprop2d  17767  lssintcl  17805  prdslmodd  17810  islmhm2  17879  islbs3  17996  ofco2  19120  mdetmul  19292  restopnb  19843  regsep2  20044  iuncon  20095  blsscls2  21173  met2ndci  21191  xrsblre  21482  legso  24186  colline  24231  tglowdim2ln  24233  f1otrg  24376  f1otrge  24377  ax5seglem4  24437  ax5seglem5  24438  axcontlem4  24472  axcontlem8  24476  axcontlem9  24477  axcontlem10  24478  eengtrkg  24490  el2wlksotot  25084  rusgranumwlks  25158  extwwlkfablem1  25276  submomnd  27934  ogrpaddltbi  27943  erdszelem8  28906  btwncomim  29891  btwnswapid  29895  broutsideof3  30004  outsideoftr  30007  outsidele  30010  mendassa  31384  3adantlr3  31657  ioondisj2  31764  ioondisj1  31765  subsubelfzo0  32712  ply1mulgsumlem2  33241  lincresunit3lem2  33335  cvrletrN  35395  ltltncvr  35544  atcvrj2b  35553  2at0mat0  35646  paddasslem11  35951  pmod1i  35969  lautcvr  36213  tendoplass  36906  tendodi1  36907  tendodi2  36908  cdlemk34  37033