Theorem simprr1 1036

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

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

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 967

This theorem is referenced by:  sqrmo  12733  psgnunilem2  15992  haust1  18936  cnhaus  18938  isreg2  18961  llynlly  19061  restnlly  19066  llyrest  19069  llyidm  19072  nllyidm  19073  cldllycmp  19079  txlly  19189  txnlly  19190  pthaus  19191  txhaus  19200  txkgen  19205  xkohaus  19206  xkococnlem  19212  hauspwpwf1  19540  itg2add  21217  ulmdvlem3  21847  ax5seglem6  23148  conpcon  27093  cvmliftmolem2  27140  cvmlift2lem10  27170  cvmlift3lem2  27178  cvmlift3lem8  27184  broutsideof3  28126  icodiamlt  29132  mpaaeu  29478  stoweidlem35  29801  stoweidlem56  29822  stoweidlem59  29825  frg2woteqm  30623  numclwlk1lem2f  30656  numclwwlk5  30676  paddasslem10  33366  lhpexle2lem  33546  lhpexle3lem  33548  cdlemj3  34360  cdlemkid4  34471