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  5365  fcof1  5865  mpo0  6028  eroveu  6726  sbthlemi6  7079  sbthlemi8  7081  addcmpblnq  7500  mulcmpblnq  7501  ordpipqqs  7507  addcmpblnq0  7576  mulcmpblnq0  7577  nnnq0lem1  7579  prarloclemcalc  7635  addlocpr  7669  distrlem4prl  7717  distrlem4pru  7718  ltpopr  7728  addcmpblnr  7872  mulcmpblnrlemg  7873  mulcmpblnr  7874  prsrlem1  7875  ltsrprg  7880  apreap  8680  apreim  8696  aptap  8743  divdivdivap  8806  divmuleqap  8810  divadddivap  8820  divsubdivap  8821  ledivdiv  8983  lediv12a  8987  exbtwnz  10415  seq3caopr  10662  seqcaoprg  10663  leexp2r  10760  zfz1iso  11008  ccatsymb  11081  wrd2ind  11199  recvguniq  11381  rsqrmo  11413  summodclem2  11768  prodmodc  11964  qredeu  12494  pw2dvdseu  12565  pcadd  12738  mhmpropd  13373  issubmd  13381  grprcan  13444  isnsg3  13618  ghmpreima  13677  rngpropd  13792  ringpropd  13875  lmodvsmmulgdi  14160  lmodprop2d  14185  lss1d  14220  epttop  14637  txdis1cn  14825  metequiv2  15043  mulc1cncf  15136  cncfmptc  15143  cncfmptid  15144  addccncf  15147  negcncf  15152  dedekindicclemicc  15179  mpodvdsmulf1o  15537  2sqlem5  15671  2sqlem9  15676