Theorem simprr3 1111

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

Assertion

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

Proof of Theorem simprr3

Step	Hyp	Ref	Expression
1		simpr3 1069	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ch )
2	1	adantl 482	1 |- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )

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:  el2xptp0  7212  icodiamlt  14174  psgnunilem2  17915  srgbinom  18545  psgndiflemA  19947  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  fusgrfis  26222  wwlksnextfun  26793  umgr2wlkon  26846  connpconn  31217  cvmlift3lem2  31302  cvmlift3lem8  31308  noprefixmo  31848  nosupno  31849  scutbdaybnd  31921  ifscgr  32151  broutsideof3  32233  unblimceq0  32498  paddasslem10  35115  lhpexle2lem  35295  lhpexle3lem  35297  mpaaeu  37720  stoweidlem35  40252  stoweidlem56  40273  stoweidlem59  40276