Theorem simp1rr 1054

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

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:  f1imass  6079  smo11  6928  zsupss  11048  lsmcv  17337  lspsolvlem  17338  nrmr0reg  19447  plyadd  21811  plymul  21812  coeeu  21819  ax5seglem6  23325  archiabl  26353  sseqval  26908  wsuclem  27899  btwnconn1lem1  28255  btwnconn1lem2  28256  btwnconn1lem12  28266  pellex  29317  mat2pmatghm  31196  mat2pmatmul  31197  lshpsmreu  33063  1cvratlt  33427  llnle  33471  lvolex3N  33491  lnjatN  33733  lncvrat  33735  lncmp  33736  cdlemd6  34156  cdlemk19ylem  34883