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  5402  fcof1  5906  mpo0  6073  eroveu  6771  sbthlemi6  7125  sbthlemi8  7127  addcmpblnq  7550  mulcmpblnq  7551  ordpipqqs  7557  addcmpblnq0  7626  mulcmpblnq0  7627  nnnq0lem1  7629  prarloclemcalc  7685  addlocpr  7719  distrlem4prl  7767  distrlem4pru  7768  ltpopr  7778  addcmpblnr  7922  mulcmpblnrlemg  7923  mulcmpblnr  7924  prsrlem1  7925  ltsrprg  7930  apreap  8730  apreim  8746  aptap  8793  divdivdivap  8856  divmuleqap  8860  divadddivap  8870  divsubdivap  8871  ledivdiv  9033  lediv12a  9037  exbtwnz  10465  seq3caopr  10712  seqcaoprg  10713  leexp2r  10810  zfz1iso  11058  ccatsymb  11132  wrd2ind  11250  swrdccat  11262  recvguniq  11501  rsqrmo  11533  summodclem2  11888  prodmodc  12084  qredeu  12614  pw2dvdseu  12685  pcadd  12858  mhmpropd  13494  issubmd  13502  grprcan  13565  isnsg3  13739  ghmpreima  13798  rngpropd  13913  ringpropd  13996  lmodvsmmulgdi  14281  lmodprop2d  14306  lss1d  14341  epttop  14758  txdis1cn  14946  metequiv2  15164  mulc1cncf  15257  cncfmptc  15264  cncfmptid  15265  addccncf  15268  negcncf  15273  dedekindicclemicc  15300  mpodvdsmulf1o  15658  2sqlem5  15792  2sqlem9  15797