Theorem simplr1 1039

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

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

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 976

This theorem is referenced by:  soltmin  5396  frfi  7767  wemappo  7977  iccsplit  11662  ccatswrd  12660  sqrmo  13064  pcdvdstr  14276  vdwlem12  14387  mreexexlem4d  14921  iscatd2  14955  oppccomfpropd  14999  resssetc  15293  resscatc  15306  mod1ile  15609  mod2ile  15610  prdsmndd  15827  grprcan  15957  prdsringd  17135  lmodprop2d  17446  lssintcl  17484  prdslmodd  17489  islmhm2  17558  islbs3  17675  ofco2  18826  mdetmul  18998  restopnb  19549  regsep2  19750  iuncon  19802  blsscls2  20880  met2ndci  20898  xrsblre  21189  legso  23857  colline  23902  tglowdim2ln  23904  f1otrg  24046  f1otrge  24047  ax5seglem4  24107  ax5seglem5  24108  axcontlem4  24142  axcontlem8  24146  axcontlem9  24147  axcontlem10  24148  eengtrkg  24160  el2wlksotot  24754  rusgranumwlks  24828  extwwlkfablem1  24946  submomnd  27573  ogrpaddltbi  27582  erdszelem8  28515  btwncomim  29638  btwnswapid  29642  broutsideof3  29751  outsideoftr  29754  outsidele  29757  mendassa  31119  3adantlr3  31371  ioondisj2  31461  ioondisj1  31462  subsubelfzo0  32176  ply1mulgsumlem2  32717  lincresunit3lem2  32811  cvrletrN  34732  ltltncvr  34881  atcvrj2b  34890  2at0mat0  34983  paddasslem11  35288  pmod1i  35306  lautcvr  35550  tendoplass  36243  tendodi1  36244  tendodi2  36245  cdlemk34  36370