Theorem simp-4r 548

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 540	. 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  550  fimax2gtri  7196  finexdc  7197  fissfi  7253  dcfi  7305  difinfsn  7430  nnnninfeq2  7459  nninfisol  7463  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  suplocexprlemru  8076  suplocsrlemb  8163  suplocsrlem  8165  aptap  8968  supinfneg  9974  infsupneg  9975  xaddf  10225  xaddval  10226  nn0ltexp2  11125  hashunlem  11222  swrdccatin1  11475  reuccatpfxs1  11497  xrmaxiflemcl  11989  xrmaxiflemlub  11992  xrmaxltsup  12002  sumeq2  12103  fsumconst  12199  prodeq2  12302  fprodconst  12365  nninfctlemfo  12795  sgrpidmndm  13710  mhmmnd  13896  ghmcmn  14108  prdsval  14150  issrg  14243  cncnp  15254  neitx  15292  dedekindeulemlu  15645  suplociccreex  15648  dedekindicclemlu  15654  cnplimclemr  15693  limccnp2cntop  15701  logbgcd1irrap  15995  lgsval  16037  usgr1vr  16403  pw1ndom3  16934