Theorem simp1rr 1063

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

Assertion

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

Proof of Theorem simp1rr

Step	Hyp	Ref	Expression
1		simprr 757	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ps )
2	1	3ad2ant1 1018	1 |- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ps )

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:  f1imass  6157  smo11  7037  zsupss  11180  lsmcv  17661  lspsolvlem  17662  mat2pmatghm  19104  mat2pmatmul  19105  nrmr0reg  20123  plyadd  22487  plymul  22488  coeeu  22495  ax5seglem6  24109  archiabl  27615  sseqval  28200  wsuclem  29356  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem12  29723  pellex  30746  limcperiod  31542  lshpsmreu  34568  1cvratlt  34932  llnle  34976  lvolex3N  34996  lnjatN  35238  lncvrat  35240  lncmp  35241  cdlemd6  35662  cdlemk19ylem  36390