Theorem simp1lr 1125

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp1lr	|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ps )

Proof of Theorem simp1lr

Step	Hyp	Ref	Expression
1		simplr 792	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ps )
2	1	3ad2ant1 1082	1 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  lspsolvlem  19142  dmatcrng  20308  scmatcrng  20327  1marepvsma1  20389  mdetunilem7  20424  mat2pmatghm  20535  pmatcollpwscmatlem2  20595  mp2pm2mplem4  20614  ax5seg  25818  clwwnisshclwwsn  26930  measinblem  30283  btwnconn1lem13  32206  athgt  34742  llnle  34804  lplnle  34826  lhpexle1  35294  lhpat3  35332  tendoicl  36084  cdlemk55b  36248  pellex  37399  ssfiunibd  39523  mullimc  39848  mullimcf  39855  icccncfext  40100  etransclem32  40483