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  5924  mpo0  6091  eroveu  6795  sbthlemi6  7161  sbthlemi8  7163  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prarloclemcalc  7722  addlocpr  7756  distrlem4prl  7804  distrlem4pru  7805  ltpopr  7815  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  ltsrprg  7967  apreap  8767  apreim  8783  aptap  8830  divdivdivap  8893  divmuleqap  8897  divadddivap  8907  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  exbtwnz  10511  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  zfz1iso  11106  ccatsymb  11183  wrd2ind  11308  swrdccat  11320  recvguniq  11573  rsqrmo  11605  summodclem2  11961  prodmodc  12157  qredeu  12687  pw2dvdseu  12758  pcadd  12931  mhmpropd  13567  issubmd  13575  grprcan  13638  isnsg3  13812  ghmpreima  13871  rngpropd  13987  ringpropd  14070  lmodvsmmulgdi  14356  lmodprop2d  14381  lss1d  14416  epttop  14833  txdis1cn  15021  metequiv2  15239  mulc1cncf  15332  cncfmptc  15339  cncfmptid  15340  addccncf  15343  negcncf  15348  dedekindicclemicc  15375  mpodvdsmulf1o  15733  2sqlem5  15867  2sqlem9  15872