Theorem simprr2 1110

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

Assertion

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

Proof of Theorem simprr2

Step	Hyp	Ref	Expression
1		simpr2 1068	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ps )
2	1	adantl 482	1 |- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> 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  psgnunilem2  17915  haust1  21156  cnhaus  21158  isreg2  21181  llynlly  21280  restnlly  21285  llyrest  21288  llyidm  21291  nllyidm  21292  cldllycmp  21298  txlly  21439  txnlly  21440  pthaus  21441  txhaus  21450  txkgen  21455  xkohaus  21456  xkococnlem  21462  cmetcaulem  23086  itg2add  23526  ulmdvlem3  24156  ax5seglem6  25814  n4cyclfrgr  27155  numclwlk1lem2f  27225  connpconn  31217  cvmlift3lem2  31302  cvmlift3lem8  31308  noprefixmo  31848  scutbdaybnd  31921  broutsideof3  32233  unblimceq0  32498  paddasslem10  35115  lhpexle2lem  35295  lhpexle3lem  35297  stoweidlem35  40252  stoweidlem56  40273  stoweidlem59  40276