Theorem simp1rr 1071

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 764	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ps )
2	1	3ad2ant1 1026	1 |- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  f1imass  6124  smo11  7038  zsupss  11204  lsmcv  18307  lspsolvlem  18308  mat2pmatghm  19696  mat2pmatmul  19697  nrmr0reg  20706  plyadd  23113  plymul  23114  coeeu  23121  ax5seglem6  24906  archiabl  28466  mdetpmtr1  28601  sseqval  29173  wsuclem  30459  btwnconn1lem1  30803  btwnconn1lem2  30804  btwnconn1lem12  30814  lshpsmreu  32587  1cvratlt  32951  llnle  32995  lvolex3N  33015  lnjatN  33257  lncvrat  33259  lncmp  33260  cdlemd6  33681  cdlemk19ylem  34409  pellex  35592  limcperiod  37591