Theorem simprll 539

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antrl 490	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> 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:  imain  5443  fcof1  5962  mpo0  6131  eroveu  6873  sbthlemi6  7245  sbthlemi8  7247  suppeqfsuppbi  7261  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prarloclemcalc  7833  addlocpr  7867  distrlem4prl  7915  distrlem4pru  7916  ltpopr  7926  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  ltsrprg  8078  apreap  8878  apreim  8894  aptap  8941  divdivdivap  9004  divmuleqap  9008  divadddivap  9018  divsubdivap  9019  ledivdiv  9181  lediv12a  9185  exbtwnz  10634  seq3caopr  10881  seqcaoprg  10882  leexp2r  10979  zfz1iso  11238  ccatsymb  11315  wrd2ind  11440  swrdccat  11452  recvguniq  11705  rsqrmo  11737  summodclem2  12093  prodmodc  12289  qredeu  12819  pw2dvdseu  12890  pcadd  13063  mhmpropd  13721  issubmd  13729  grprcan  13792  isnsg3  13960  ghmpreima  14019  rngpropd  14194  ringpropd  14281  lmodvsmmulgdi  14597  lmodprop2d  14622  lss1d  14657  epttop  15081  txdis1cn  15269  metequiv2  15487  mulc1cncf  15580  cncfmptc  15587  cncfmptid  15588  addccncf  15591  negcncf  15596  dedekindicclemicc  15623  mpodvdsmulf1o  15984  2sqlem5  16118  2sqlem9  16123