Theorem simprlr 544

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprlr	|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antrl 494	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )

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  fliftfun  6005  sbthlemi6  7286  sbthlemi8  7288  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  enq0tr  7808  addcmpblnq0  7817  mulcmpblnq0  7818  nnnq0lem1  7820  addnq0mo  7821  mulnq0mo  7822  prarloclemcalc  7876  addlocpr  7910  distrlem4prl  7958  distrlem4pru  7959  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  addsrmo  8117  mulsrmo  8118  ltsrprg  8121  apreap  8924  apreim  8940  aptap  8987  divdivdivap  9052  divsubdivap  9067  ledivdiv  9229  lediv12a  9233  exbtwnz  10702  seq3caopr  10953  seqcaoprg  10954  leexp2r  11051  hashfibclem  11304  hashf1lem1  11307  hashf1lem2  11308  zfz1iso  11315  wrd2ind  11517  swrdccat  11529  recvguniq  11783  rsqrmo  11815  summodclem2  12174  prodmodclem2  12369  prodmodc  12370  qredeu  12900  pwbdvdseu  12972  nnmaxpwlemparts  12977  pcadd  13148  ballotfilemfc0  13290  ballotfilemfcc  13291  mhmpropd  13832  grprcan  13901  isnsg3  14069  ghmpreima  14128  rngpropd  14361  ringpropd  14450  islmodd  14738  lmodprop2d  14794  lss1d  14829  assamulgscmlem2  15151  mvrf1fi  15231  mplsubgfilemcl  15246  epttop  15349  txdis1cn  15537  metequiv2  15755  cncfmptc  15855  cncfmptid  15856  addccncf  15859  negcncf  15864  dedekindicclemicc  15891  mpodvdsmulf1o  16317  2sqlem5  16476  2sqlem9  16481