Theorem simprll 537

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  5403  fcof1  5913  mpo0  6080  eroveu  6781  sbthlemi6  7140  sbthlemi8  7142  addcmpblnq  7565  mulcmpblnq  7566  ordpipqqs  7572  addcmpblnq0  7641  mulcmpblnq0  7642  nnnq0lem1  7644  prarloclemcalc  7700  addlocpr  7734  distrlem4prl  7782  distrlem4pru  7783  ltpopr  7793  addcmpblnr  7937  mulcmpblnrlemg  7938  mulcmpblnr  7939  prsrlem1  7940  ltsrprg  7945  apreap  8745  apreim  8761  aptap  8808  divdivdivap  8871  divmuleqap  8875  divadddivap  8885  divsubdivap  8886  ledivdiv  9048  lediv12a  9052  exbtwnz  10482  seq3caopr  10729  seqcaoprg  10730  leexp2r  10827  zfz1iso  11076  ccatsymb  11150  wrd2ind  11270  swrdccat  11282  recvguniq  11521  rsqrmo  11553  summodclem2  11908  prodmodc  12104  qredeu  12634  pw2dvdseu  12705  pcadd  12878  mhmpropd  13514  issubmd  13522  grprcan  13585  isnsg3  13759  ghmpreima  13818  rngpropd  13933  ringpropd  14016  lmodvsmmulgdi  14302  lmodprop2d  14327  lss1d  14362  epttop  14779  txdis1cn  14967  metequiv2  15185  mulc1cncf  15278  cncfmptc  15285  cncfmptid  15286  addccncf  15289  negcncf  15294  dedekindicclemicc  15321  mpodvdsmulf1o  15679  2sqlem5  15813  2sqlem9  15818