Theorem simprr1 1043

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

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

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 974

This theorem is referenced by:  sqrmo  13059  psgnunilem2  16389  haust1  19719  cnhaus  19721  isreg2  19744  llynlly  19844  restnlly  19849  llyrest  19852  llyidm  19855  nllyidm  19856  cldllycmp  19862  txlly  20003  txnlly  20004  pthaus  20005  txhaus  20014  txkgen  20019  xkohaus  20020  xkococnlem  20026  hauspwpwf1  20354  itg2add  22032  ulmdvlem3  22662  ax5seglem6  24102  frg2woteqm  24924  numclwlk1lem2f  24957  numclwwlk5  24977  conpcon  28546  cvmliftmolem2  28593  cvmlift2lem10  28623  cvmlift3lem2  28631  cvmlift3lem8  28637  broutsideof3  29744  icodiamlt  30724  mpaaeu  31068  stoweidlem35  31702  stoweidlem56  31723  stoweidlem59  31726  paddasslem10  35255  lhpexle2lem  35435  lhpexle3lem  35437  cdlemj3  36251  cdlemkid4  36362