Theorem simp-4r 544

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 536	. 2 |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  simp-5r  546  fimax2gtri  7159  finexdc  7160  fissfi  7216  dcfi  7268  difinfsn  7391  nnnninfeq2  7420  nninfisol  7424  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  suplocexprlemru  8034  suplocsrlemb  8121  suplocsrlem  8123  aptap  8924  supinfneg  9927  infsupneg  9928  xaddf  10177  xaddval  10178  nn0ltexp2  11071  hashunlem  11168  swrdccatin1  11417  reuccatpfxs1  11439  xrmaxiflemcl  11930  xrmaxiflemlub  11933  xrmaxltsup  11943  sumeq2  12044  fsumconst  12140  prodeq2  12243  fprodconst  12306  nninfctlemfo  12736  prdsval  13486  sgrpidmndm  13633  mhmmnd  13833  ghmcmn  14044  issrg  14109  cncnp  15095  neitx  15133  dedekindeulemlu  15486  suplociccreex  15489  dedekindicclemlu  15495  cnplimclemr  15534  limccnp2cntop  15542  logbgcd1irrap  15835  lgsval  15877  usgr1vr  16243  pw1ndom3  16764