Theorem simprl2 1107

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

Assertion

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

Proof of Theorem simprl2

Step	Hyp	Ref	Expression
1		simpl2 1065	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantl 482	1 |- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> 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:  icodiamlt  14174  issubc3  16509  clsconn  21233  txlly  21439  txnlly  21440  itg2add  23526  ftc1a  23800  f1otrg  25751  ax5seglem6  25814  axcontlem9  25852  axcontlem10  25853  clwwlksf  26915  locfinref  29908  erdszelem7  31179  noprefixmo  31848  nosupbnd2  31862  btwnconn1lem13  32206  dfsalgen2  40559