Theorem simplr1 1030

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

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

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 967

This theorem is referenced by:  soltmin  5348  frfi  7671  wemappo  7878  iccsplit  11539  ccatswrd  12472  sqrmo  12863  pcdvdstr  14064  vdwlem12  14175  mreexexlem4d  14708  iscatd2  14742  oppccomfpropd  14789  resssetc  15083  resscatc  15096  mod1ile  15398  mod2ile  15399  prdsmndd  15577  grprcan  15694  prdsrngd  16837  lmodprop2d  17140  lssintcl  17178  prdslmodd  17183  islmhm2  17252  islbs3  17369  ofco2  18469  mdetmul  18571  restopnb  18921  regsep2  19122  iuncon  19174  blsscls2  20221  met2ndci  20239  xrsblre  20530  colline  23204  tglowdim2ln  23206  f1otrg  23296  f1otrge  23297  ax5seglem4  23357  ax5seglem5  23358  axcontlem4  23392  axcontlem8  23396  axcontlem9  23397  axcontlem10  23398  eengtrkg  23410  submomnd  26345  ogrpaddltbi  26354  erdszelem8  27253  btwncomim  28211  btwnswapid  28215  broutsideof3  28324  outsideoftr  28327  outsidele  28330  mendassa  29722  subsubelfzo0  30381  el2wlksotot  30572  rusgranumwlks  30745  extwwlkfablem1  30838  ply1mulgsumlem2  31022  lincresunit3lem2  31169  cvrletrN  33281  ltltncvr  33430  atcvrj2b  33439  2at0mat0  33532  paddasslem11  33837  pmod1i  33855  lautcvr  34099  tendoplass  34790  tendodi1  34791  tendodi2  34792  cdlemk34  34917