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  12845  psgnunilem2  16105  haust1  19074  cnhaus  19076  isreg2  19099  llynlly  19199  restnlly  19204  llyrest  19207  llyidm  19210  nllyidm  19211  cldllycmp  19217  txlly  19327  txnlly  19328  pthaus  19329  txhaus  19338  txkgen  19343  xkohaus  19344  xkococnlem  19350  hauspwpwf1  19678  itg2add  21355  ulmdvlem3  21985  ax5seglem6  23317  conpcon  27260  cvmliftmolem2  27307  cvmlift2lem10  27337  cvmlift3lem2  27345  cvmlift3lem8  27351  broutsideof3  28293  icodiamlt  29301  mpaaeu  29647  stoweidlem35  29970  stoweidlem56  29991  stoweidlem59  29994  frg2woteqm  30792  numclwlk1lem2f  30825  numclwwlk5  30845  paddasslem10  33781  lhpexle2lem  33961  lhpexle3lem  33963  cdlemj3  34775  cdlemkid4  34886