Theorem simp-4r 537

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-4r	|- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		simpllr 529	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 274	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-5r  539  fimax2gtri  6879  finexdc  6880  dcfi  6958  difinfsn  7077  nnnninfeq2  7105  nninfisol  7109  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  suplocexprlemru  7681  suplocsrlemb  7768  suplocsrlem  7770  supinfneg  9554  infsupneg  9555  xaddf  9801  xaddval  9802  nn0ltexp2  10644  hashunlem  10739  xrmaxiflemcl  11208  xrmaxiflemlub  11211  xrmaxltsup  11221  sumeq2  11322  fsumconst  11417  prodeq2  11520  fprodconst  11583  sgrpidmndm  12656  cncnp  13024  neitx  13062  dedekindeulemlu  13393  suplociccreex  13396  dedekindicclemlu  13402  cnplimclemr  13432  limccnp2cntop  13440  logbgcd1irrap  13682  lgsval  13699