Theorem simprr1 1029

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

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

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 960

This theorem is referenced by:  sqrmo  12724  psgnunilem2  15980  haust1  18797  cnhaus  18799  isreg2  18822  llynlly  18922  restnlly  18927  llyrest  18930  llyidm  18933  nllyidm  18934  cldllycmp  18940  txlly  19050  txnlly  19051  pthaus  19052  txhaus  19061  txkgen  19066  xkohaus  19067  xkococnlem  19073  hauspwpwf1  19401  itg2add  21078  ulmdvlem3  21751  ax5seglem6  23002  conpcon  26971  cvmliftmolem2  27018  cvmlift2lem10  27048  cvmlift3lem2  27056  cvmlift3lem8  27062  broutsideof3  28003  icodiamlt  29003  mpaaeu  29349  stoweidlem35  29673  stoweidlem56  29694  stoweidlem59  29697  frg2woteqm  30495  numclwlk1lem2f  30528  numclwwlk5  30548  paddasslem10  33043  lhpexle2lem  33223  lhpexle3lem  33225  cdlemj3  34037  cdlemkid4  34148