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  5419  fcof1  5934  mpo0  6101  eroveu  6838  sbthlemi6  7204  sbthlemi8  7206  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  addcmpblnq0  7706  mulcmpblnq0  7707  nnnq0lem1  7709  prarloclemcalc  7765  addlocpr  7799  distrlem4prl  7847  distrlem4pru  7848  ltpopr  7858  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  ltsrprg  8010  apreap  8809  apreim  8825  aptap  8872  divdivdivap  8935  divmuleqap  8939  divadddivap  8949  divsubdivap  8950  ledivdiv  9112  lediv12a  9116  exbtwnz  10556  seq3caopr  10803  seqcaoprg  10804  leexp2r  10901  zfz1iso  11151  ccatsymb  11228  wrd2ind  11353  swrdccat  11365  recvguniq  11618  rsqrmo  11650  summodclem2  12006  prodmodc  12202  qredeu  12732  pw2dvdseu  12803  pcadd  12976  mhmpropd  13612  issubmd  13620  grprcan  13683  isnsg3  13857  ghmpreima  13916  rngpropd  14032  ringpropd  14115  lmodvsmmulgdi  14402  lmodprop2d  14427  lss1d  14462  epttop  14884  txdis1cn  15072  metequiv2  15290  mulc1cncf  15383  cncfmptc  15390  cncfmptid  15391  addccncf  15394  negcncf  15399  dedekindicclemicc  15426  mpodvdsmulf1o  15787  2sqlem5  15921  2sqlem9  15926