Theorem simprr1 1005

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 963	. 2 |- ( ( th /\ ( ph /\ ps /\ ch ) ) -> ph )
2	1	adantl 453	1 |- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  sqrmo  12012  haust1  17370  cnhaus  17372  isreg2  17395  llynlly  17493  restnlly  17498  llyrest  17501  llyidm  17504  nllyidm  17505  cldllycmp  17511  txlly  17621  txnlly  17622  pthaus  17623  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  hauspwpwf1  17972  itg2add  19604  ulmdvlem3  20271  conpcon  24875  cvmliftmolem2  24922  cvmlift2lem10  24952  cvmlift3lem2  24960  cvmlift3lem8  24966  ax5seglem6  25777  broutsideof3  25964  icodiamlt  26773  mpaaeu  27223  psgnunilem2  27286  stoweidlem35  27651  stoweidlem56  27672  stoweidlem59  27675  frg2woteqm  28162  paddasslem10  30311  lhpexle2lem  30491  lhpexle3lem  30493  cdlemj3  31305  cdlemkid4  31416

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938