Theorem simprll 543

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 494	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  imain  5466  fcof1  5992  mpo0  6161  eroveu  6905  sbthlemi6  7286  sbthlemi8  7288  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  addcmpblnq0  7816  mulcmpblnq0  7817  nnnq0lem1  7819  prarloclemcalc  7875  addlocpr  7909  distrlem4prl  7957  distrlem4pru  7958  ltpopr  7968  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  prsrlem1  8115  ltsrprg  8120  apreap  8923  apreim  8939  aptap  8986  divdivdivap  9051  divmuleqap  9055  divadddivap  9065  divsubdivap  9066  ledivdiv  9228  lediv12a  9232  exbtwnz  10701  seq3caopr  10952  seqcaoprg  10953  leexp2r  11050  hashf1lem1  11306  hashf1lem2  11307  zfz1iso  11314  ccatsymb  11391  wrd2ind  11516  swrdccat  11528  recvguniq  11782  rsqrmo  11814  summodclem2  12173  prodmodc  12369  qredeu  12899  pwbdvdseu  12971  pcadd  13147  mhmpropd  13831  issubmd  13839  grprcan  13900  isnsg3  14068  ghmpreima  14127  rngpropd  14360  ringpropd  14449  lmodvsmmulgdi  14768  lmodprop2d  14793  lss1d  14828  assamulgscmlem2  15150  mvrf1fi  15219  mplsubgfilemcl  15232  epttop  15333  txdis1cn  15521  metequiv2  15739  mulc1cncf  15832  cncfmptc  15839  cncfmptid  15840  addccncf  15843  negcncf  15848  dedekindicclemicc  15875  mpodvdsmulf1o  16301  2sqlem5  16460  2sqlem9  16465