Theorem simprr1 1039

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

Assertion

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

Proof of Theorem simprr1

Step	Hyp	Ref	Expression
1		simpr1 997	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantl 466	1 |- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 968

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 970

This theorem is referenced by:  sqrmo  13035  psgnunilem2  16309  haust1  19612  cnhaus  19614  isreg2  19637  llynlly  19737  restnlly  19742  llyrest  19745  llyidm  19748  nllyidm  19749  cldllycmp  19755  txlly  19865  txnlly  19866  pthaus  19867  txhaus  19876  txkgen  19881  xkohaus  19882  xkococnlem  19888  hauspwpwf1  20216  itg2add  21894  ulmdvlem3  22524  ax5seglem6  23906  conpcon  28170  cvmliftmolem2  28217  cvmlift2lem10  28247  cvmlift3lem2  28255  cvmlift3lem8  28261  broutsideof3  29203  icodiamlt  30211  mpaaeu  30557  stoweidlem35  31154  stoweidlem56  31175  stoweidlem59  31178  frg2woteqm  31778  numclwlk1lem2f  31811  numclwwlk5  31831  paddasslem10  34500  lhpexle2lem  34680  lhpexle3lem  34682  cdlemj3  35494  cdlemkid4  35605