Theorem simplr1 1038

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

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973

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  df-3an 975

This theorem is referenced by:  soltmin  5412  frfi  7777  wemappo  7986  iccsplit  11665  ccatswrd  12661  sqrmo  13065  pcdvdstr  14275  vdwlem12  14386  mreexexlem4d  14919  iscatd2  14953  oppccomfpropd  15000  resssetc  15294  resscatc  15307  mod1ile  15609  mod2ile  15610  prdsmndd  15826  grprcan  15955  prdsringd  17133  lmodprop2d  17443  lssintcl  17481  prdslmodd  17486  islmhm2  17555  islbs3  17672  ofco2  18822  mdetmul  18994  restopnb  19544  regsep2  19745  iuncon  19797  blsscls2  20875  met2ndci  20893  xrsblre  21184  legso  23850  colline  23882  tglowdim2ln  23884  f1otrg  23997  f1otrge  23998  ax5seglem4  24058  ax5seglem5  24059  axcontlem4  24093  axcontlem8  24097  axcontlem9  24098  axcontlem10  24099  eengtrkg  24111  el2wlksotot  24705  rusgranumwlks  24779  extwwlkfablem1  24898  submomnd  27524  ogrpaddltbi  27533  erdszelem8  28467  btwncomim  29590  btwnswapid  29594  broutsideof3  29703  outsideoftr  29706  outsidele  29709  mendassa  31072  3adantlr3  31319  ioondisj2  31412  ioondisj1  31413  subsubelfzo0  32128  ply1mulgsumlem2  32469  lincresunit3lem2  32563  cvrletrN  34471  ltltncvr  34620  atcvrj2b  34629  2at0mat0  34722  paddasslem11  35027  pmod1i  35045  lautcvr  35289  tendoplass  35980  tendodi1  35981  tendodi2  35982  cdlemk34  36107