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  5438  fcof1  5956  mpo0  6123  eroveu  6860  sbthlemi6  7232  sbthlemi8  7234  suppeqfsuppbi  7248  addcmpblnq  7682  mulcmpblnq  7683  ordpipqqs  7689  addcmpblnq0  7758  mulcmpblnq0  7759  nnnq0lem1  7761  prarloclemcalc  7817  addlocpr  7851  distrlem4prl  7899  distrlem4pru  7900  ltpopr  7910  addcmpblnr  8054  mulcmpblnrlemg  8055  mulcmpblnr  8056  prsrlem1  8057  ltsrprg  8062  apreap  8861  apreim  8877  aptap  8924  divdivdivap  8987  divmuleqap  8991  divadddivap  9001  divsubdivap  9002  ledivdiv  9164  lediv12a  9168  exbtwnz  10610  seq3caopr  10857  seqcaoprg  10858  leexp2r  10955  zfz1iso  11213  ccatsymb  11290  wrd2ind  11415  swrdccat  11427  recvguniq  11680  rsqrmo  11712  summodclem2  12068  prodmodc  12264  qredeu  12794  pw2dvdseu  12865  pcadd  13038  mhmpropd  13679  issubmd  13687  grprcan  13750  isnsg3  13924  ghmpreima  13983  rngpropd  14099  ringpropd  14182  lmodvsmmulgdi  14471  lmodprop2d  14496  lss1d  14531  epttop  14955  txdis1cn  15143  metequiv2  15361  mulc1cncf  15454  cncfmptc  15461  cncfmptid  15462  addccncf  15465  negcncf  15470  dedekindicclemicc  15497  mpodvdsmulf1o  15858  2sqlem5  15992  2sqlem9  15997