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  5412  fcof1  5923  mpo0  6090  eroveu  6794  sbthlemi6  7160  sbthlemi8  7162  addcmpblnq  7586  mulcmpblnq  7587  ordpipqqs  7593  addcmpblnq0  7662  mulcmpblnq0  7663  nnnq0lem1  7665  prarloclemcalc  7721  addlocpr  7755  distrlem4prl  7803  distrlem4pru  7804  ltpopr  7814  addcmpblnr  7958  mulcmpblnrlemg  7959  mulcmpblnr  7960  prsrlem1  7961  ltsrprg  7966  apreap  8766  apreim  8782  aptap  8829  divdivdivap  8892  divmuleqap  8896  divadddivap  8906  divsubdivap  8907  ledivdiv  9069  lediv12a  9073  exbtwnz  10509  seq3caopr  10756  seqcaoprg  10757  leexp2r  10854  zfz1iso  11104  ccatsymb  11178  wrd2ind  11303  swrdccat  11315  recvguniq  11555  rsqrmo  11587  summodclem2  11942  prodmodc  12138  qredeu  12668  pw2dvdseu  12739  pcadd  12912  mhmpropd  13548  issubmd  13556  grprcan  13619  isnsg3  13793  ghmpreima  13852  rngpropd  13967  ringpropd  14050  lmodvsmmulgdi  14336  lmodprop2d  14361  lss1d  14396  epttop  14813  txdis1cn  15001  metequiv2  15219  mulc1cncf  15312  cncfmptc  15319  cncfmptid  15320  addccncf  15323  negcncf  15328  dedekindicclemicc  15355  mpodvdsmulf1o  15713  2sqlem5  15847  2sqlem9  15852