Theorem simplr1 999

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

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  soltmin  5232  frfi  7311  wemappo  7474  iccsplit  10985  ccatswrd  11728  sqrmo  12012  pcdvdstr  13204  vdwlem12  13315  mreexexlem4d  13827  iscatd2  13861  oppccomfpropd  13908  resssetc  14202  resscatc  14215  mod1ile  14489  mod2ile  14490  prdsmndd  14683  grprcan  14793  prdsrngd  15673  lmodprop2d  15961  lssintcl  15995  prdslmodd  16000  islmhm2  16069  islbs3  16182  restopnb  17193  regsep2  17394  iuncon  17444  blsscls2  18487  met2ndci  18505  xrsblre  18795  ofldaddlt  24194  erdszelem8  24837  ax5seglem4  25775  ax5seglem5  25776  axcontlem4  25810  axcontlem8  25814  axcontlem9  25815  axcontlem10  25816  btwncomim  25851  btwnswapid  25855  broutsideof3  25964  outsideoftr  25967  outsidele  25970  mendassa  27370  el2wlksotot  28079  cvrletrN  29756  ltltncvr  29905  atcvrj2b  29914  2at0mat0  30007  paddasslem11  30312  pmod1i  30330  lautcvr  30574  tendoplass  31265  tendodi1  31266  tendodi2  31267  cdlemk34  31392

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938