Theorem simplrr 801

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

Assertion

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

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 477	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antlr 763	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  disjxiun  4649  disjxiunOLD  4650  fsnex  6538  f1prex  6539  isotr  6586  weniso  6604  riota5f  6636  tfrlem9a  7482  oaass  7641  oeeui  7682  oaabs2  7725  resixpfo  7946  omxpenlem  8061  pw2f1olem  8064  fopwdom  8068  fofinf1o  8241  marypha1lem  8339  ordiso2  8420  oismo  8445  ixpiunwdom  8496  cantnf  8590  fseqenlem1  8847  iunfictbso  8937  dfac12lem2  8966  dfac12lem3  8967  infunsdom1  9035  infpssrlem5  9129  fin23lem24  9144  isf32lem2  9176  isf32lem4  9178  isf34lem4  9199  fin1a2lem12  9233  fin1a2lem13  9234  ttukeylem6  9336  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  winalim2  9518  wunex2  9560  tskord  9602  prlem934  9855  mulcmpblnr  9892  dedekind  10200  addid1  10216  cnegex  10217  negeu  10271  add20  10540  divdivdiv  10726  ltmul12a  10879  lemul12a  10881  lediv12a  10916  supaddc  10990  supmul1  10992  cru  11012  uzwo3  11783  xleadd1a  12083  xmullem  12094  xmulgt0  12113  xlemul1a  12118  ixxun  12191  ixxss12  12195  ioodisj  12302  fz0fzelfz0  12445  mulexpz  12900  leexp1a  12919  expmulnbnd  12996  hashf1  13241  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  reuccats1  13480  abs3lem  14078  rexanre  14086  cau3lem  14094  limsupgre  14212  limsupbnd2  14214  o1lo1  14268  rlimclim1  14276  rlimclim  14277  rlimcn1  14319  rlimcn2  14321  o1of2  14343  o1rlimmul  14349  lo1add  14357  lo1mul  14358  isercolllem1  14395  climcau  14401  caucvgrlem  14403  caucvgb  14410  summolem2  14447  summo  14448  modfsummod  14526  o1fsum  14545  prodmolem2  14665  addmodlteqALT  15047  rpdvds  15374  isprm5  15419  isprm6  15426  pclem  15543  pcqmul  15558  pcexp  15564  pcneg  15578  pcprmpw2  15586  pcadd  15593  pcmpt  15596  4sqlem13  15661  vdwlem2  15686  vdwlem7  15691  vdwlem12  15696  ramval  15712  ramub2  15718  ramz2  15728  ramcl  15733  cshwshashlem2  15803  imasval  16171  imasdsval  16175  mreexexd  16308  mreexexdOLD  16309  acsfn  16320  issubc3  16509  idfucl  16541  funcres2c  16561  isnat  16607  fucpropd  16637  xpcval  16817  xpcco  16823  prfval  16839  evlf2  16858  evlfcl  16862  curf12  16867  curf1cl  16868  curf2  16869  curfcl  16872  curf2ndf  16887  hof2val  16896  hofcl  16899  hofpropd  16907  yonedalem4a  16915  yonedainv  16921  drsdirfi  16938  pospo  16973  poslubmo  17146  posglbmo  17147  isipodrs  17161  acsinfd  17180  gsumvalx  17270  gsumpropd2lem  17273  ismndd  17313  mndpropd  17316  mhmeql  17364  mrcmndind  17366  frmdup3lem  17403  mhmmnd  17537  issubg4  17613  ssnmz  17636  conjnmzb  17695  f1otrspeq  17867  psgneu  17926  pgpfi  18020  sylow2blem3  18037  slwhash  18039  fislw  18040  sylow3lem2  18043  lsmdisj2  18095  pj1eu  18109  efgredlem  18160  frgpuplem  18185  gexex  18256  frgpnabl  18278  dprdfadd  18419  dpjidcl  18457  pgpfac1lem3  18476  pgpfaclem3  18482  ablfac2  18488  ringpropd  18582  islmhm2  19038  lmhmpropd  19073  lbsextlem4  19161  assapropd  19327  psrval  19362  evlslem1  19515  prmirredlem  19841  psgndiflemA  19947  lsmcss  20036  uvcf1  20131  frlmsslsp  20135  frlmup1  20137  mamucl  20207  mamuass  20208  mamudi  20209  mamudir  20210  mamuvs1  20211  mamuvs2  20212  mamulid  20247  mamurid  20248  dmatsubcl  20304  dmatmulcl  20306  scmatscm  20319  marrepval  20368  marepveval  20374  mdetunilem7  20424  gsummatr01lem4  20464  cpmatmcllem  20523  mat2pmatf1  20534  mat2pmatlin  20540  decpmatmul  20577  pm2mpmhmlem2  20624  chpidmat  20652  pptbas  20812  toponmre  20897  restbas  20962  iscncl  21073  cnrest2  21090  cnpdis  21097  lmcnp  21108  dishaus  21186  cmpcovf  21194  tgcmp  21204  dfconn2  21222  clsconn  21233  2ndcctbss  21258  dis2ndc  21263  1stccnp  21265  islly2  21287  cldllycmp  21298  locfincmp  21329  comppfsc  21335  kgentopon  21341  txcls  21407  ptpjopn  21415  dfac14  21421  xkoccn  21422  txcnp  21423  txcmpb  21447  txlm  21451  xkopt  21458  xkoco1cn  21460  xkoco2cn  21461  qtopcn  21517  qtoprest  21520  regr1lem2  21543  xkocnv  21617  qtophmeo  21620  fmfnfmlem4  21761  hausflim  21785  hauspwpwf1  21791  fclscmp  21834  alexsublem  21848  alexsubALTlem2  21852  alexsubALTlem3  21853  ptcmplem3  21858  ptcmplem4  21859  ptcmplem5  21860  cnextfun  21868  tmdgsum2  21900  symgtgp  21905  tsmsval2  21933  tsmsgsum  21942  utoptop  22038  ismet2  22138  blin  22226  metss2lem  22316  methaus  22325  met1stc  22326  met2ndci  22327  prdsxmslem2  22334  metcnp3  22345  metcnpi3  22351  metustto  22358  metustfbas  22362  nlmvscn  22491  nrginvrcn  22496  xrsxmet  22612  reconnlem1  22629  reconn  22631  xrge0tsms  22637  xmetdcn2  22640  metdscn  22659  addcnlem  22667  fsumcn  22673  cnheiborlem  22753  cnheibor  22754  bndth  22757  lebnum  22763  nmoleub2lem2  22916  ipcn  23045  iscmet3  23091  caubl  23106  rrxdstprj1  23192  minveclem3b  23199  minveclem7  23206  pjthlem2  23209  pmltpc  23219  volfiniun  23315  ioombl1  23330  dyadss  23362  dyaddisjlem  23363  dyadmax  23366  dyadmbllem  23367  opnmbllem  23369  itg1addlem2  23464  itg10a  23477  mbfi1fseqlem6  23487  itg2seq  23509  itg2monolem1  23517  itg2gt0  23527  itgfsum  23593  limcfval  23636  ellimc2  23641  ellimc3  23643  limcres  23650  limciun  23658  dvres  23675  dveflem  23742  rolle  23753  dvlip2  23758  c1liplem1  23759  dvgt0lem1  23765  dvgt0  23767  dvlt0  23768  dvne0  23774  dvfsumrlimge0  23793  ftc1lem6  23804  itgsubst  23812  mdegmullem  23838  ply1domn  23883  ply1divex  23896  fta1g  23927  fta1b  23929  plyf  23954  dgrlem  23985  coeid  23994  plydivalg  24054  aannenlem1  24083  aalioulem3  24089  aalioulem6  24092  abelthlem8  24193  efif1olem4  24291  chordthm  24564  xrlimcnp  24695  jensen  24715  lgamcvglem  24766  lgamcvg2  24781  sqf11  24865  fsumvma2  24939  perfectlem2  24955  lgsdilem  25049  lgsquad2lem2  25110  lgsquad3  25112  2sqlem5  25147  2sqlem9  25152  2sqb  25157  rpvmasumlem  25176  dchrisum0flb  25199  dchrisum0  25209  pntpbnd  25277  pntibndlem3  25281  pntleml  25300  legov  25480  legtrid  25486  tglinethru  25531  tglnpt2  25536  tglineintmo  25537  mirreu3  25549  perpcom  25608  colperpexlem3  25624  mideu  25630  opphllem1  25639  hlpasch  25648  lnopp2hpgb  25655  trgcopy  25696  brcgr  25780  brbtwn2  25785  colinearalg  25790  axsegcon  25807  axeuclidlem  25842  axcontlem9  25852  ecgrtg  25863  elntg  25864  eengtrkg  25865  upgr1eopALT  26012  usgredg4  26109  subuhgr  26178  subumgr  26180  usgr2wspthon  26858  eupth2lems  27098  n4cyclfrgr  27155  vacn  27549  blocni  27660  ubthlem3  27728  minvecolem7  27739  chocunii  28160  pjhthmo  28161  pjhthlem2  28251  kbass5  28979  mdsymlem5  29266  foresf1o  29343  fcobij  29500  xrofsup  29533  archirngz  29743  archiabllem2a  29748  xrge0tsmsd  29785  isarchiofld  29817  smatrcl  29862  reff  29906  ordtconnlem1  29970  qqhval2  30026  volmeas  30294  fiunelcarsg  30378  ballotlemfc0  30554  ballotlemfcc  30555  signstfvneq0  30649  derangenlem  31153  erdsze2lem1  31185  pconnconn  31213  connpconn  31217  cvxsconn  31225  cvmliftmolem2  31264  cvmliftmo  31266  cvmlift2lem10  31294  cvmlift2lem12  31296  cvmlift3lem7  31307  mrsubff1  31411  msubff1  31453  poseq  31750  nolt02o  31845  noprefixmo  31848  nosupbnd2  31862  noetalem3  31865  noetalem5  31867  conway  31910  slerec  31923  ifscgr  32151  cgrxfr  32162  btwnconn1lem13  32206  btwnconn1lem14  32207  outsideofeq  32237  ellines  32259  finminlem  32312  fnejoin2  32364  unbdqndv2  32502  poimirlem13  33422  poimirlem14  33423  poimirlem32  33441  opnmbllem0  33445  mblfinlem3  33448  itg2addnclem  33461  itg2addnc  33464  ftc1cnnc  33484  upixp  33524  filbcmb  33535  sstotbnd2  33573  isbnd3  33583  prdsbnd2  33594  cntotbnd  33595  ismtyima  33602  bfp  33623  rrncmslem  33631  unichnidl  33830  lshpcmp  34275  islshpat  34304  lfl0f  34356  ishlat3N  34641  3dim1  34753  islvol5  34865  lvoli2  34867  lncvrelatN  35067  pclfinclN  35236  pexmidlem8N  35263  idltrn  35436  cdleme42keg  35774  cdleme42mgN  35776  cdlemf2  35850  cdlemg2cex  35879  trlcoat  36011  dihopelvalcpre  36537  dih1dimatlem  36618  dihjatcclem4  36710  lcfl7N  36790  lcfrlem9  36839  mapdh9a  37079  hdmapglem7  37221  nacsfix  37275  mzpsubst  37311  mzpcompact2lem  37314  eldioph2lem2  37324  eldioph2  37325  eldioph2b  37326  diophin  37336  diophun  37337  irrapxlem3  37388  irrapxlem5  37390  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrdich  37433  pell1qrge1  37434  pell1qrgaplem  37437  monotuz  37506  rpexpmord  37513  acongtr  37545  acongrep  37547  jm2.23  37563  jm2.26a  37567  jm2.26lem3  37568  jm2.26  37569  jm2.27  37575  wepwsolem  37612  fnwe2lem2  37621  kelac1  37633  kercvrlsm  37653  hbtlem5  37698  hbt  37700  mpaaeu  37720  rfovcnvf1od  38298  cncmpmax  39191  rfcnnnub  39195  disjxp1  39238  iccintsng  39749  fprodcn  39832  lptioo2  39863  lptioo1  39864  limclner  39883  stoweidlem31  40248  stoweidlem34  40251  stoweidlem35  40252  stoweidlem49  40266  stoweidlem59  40276  stoweidlem62  40279  fourierdlem60  40383  fourierdlem61  40384  fourierdlem87  40410  iundjiun  40677  ismeannd  40684  hoidmvle  40814  smfsuplem2  41018  reuccatpfxs1  41434  perfectALTVlem2  41631  mogoldbb  41673  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  mgmhmeql  41803  mndpsuppss  42152  scmsuppss  42153  lindslinindsimp2lem5  42251  elfzolborelfzop1  42309  elbigolo1  42351