Theorem simpr3 1069

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

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

Proof of Theorem simpr3

Step	Hyp	Ref	Expression
1		simp3 1063	. 2 |- ( ( ps /\ ch /\ th ) -> th )
2	1	adantl 482	1 |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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  df-3an 1039

This theorem is referenced by:  simplr3  1105  simprr3  1111  simp1r3  1159  simp2r3  1165  simp3r3  1171  3anandis  1434  funopsn  6413  fpr2g  6475  isopolem  6595  fr3nr  6979  suppfnss  7320  elfir  8321  intrnfi  8322  fisupcl  8375  cnfcomlem  8596  ackbij1lem15  9056  pwfseqlem4a  9483  pwfseqlem4  9484  eluzuzle  11696  xlesubadd  12093  elioc2  12236  elico2  12237  elicc2  12238  fseq1p1m1  12414  ccatswrd  13456  tanadd  14897  dvds2ln  15014  prmgaplem5  15759  prmgaplem8  15762  cshwsidrepsw  15800  ressress  15938  f1ovscpbl  16186  mreexexlem4d  16307  mreexexd  16308  mreexexdOLD  16309  2oppccomf  16385  fthmon  16587  fuccocl  16624  fucidcl  16625  invfuc  16634  initoeu2lem1  16664  curf2cl  16871  yonedalem4c  16917  yonedalem3  16920  pospo  16973  latjle12  17062  latjlej1  17065  latnlej2  17071  latlem12  17078  latmlem1  17081  latledi  17089  latjass  17095  latj12  17096  latj32  17097  latj13  17098  latj31  17099  latjrot  17100  latjjdi  17103  latjjdir  17104  latdisdlem  17189  prdsmndd  17323  imasmnd2  17327  imasmnd  17328  frmdmnd  17396  grpsubadd  17503  grpaddsubass  17505  grpsubsub4  17508  grppnpcan2  17509  grpnpncan  17510  grpnnncan2  17512  imasgrp2  17530  imasgrp  17531  mulgnndir  17569  mulgnndirOLD  17570  mulgnn0dir  17571  mulgnnass  17576  mulgnnassOLD  17577  mulgnn0ass  17578  mulgass  17579  pwsmulg  17587  issubg2  17609  qusgrp  17649  galcan  17737  gacan  17738  oppgmnd  17784  symggrp  17820  pmtrprfv  17873  pmtr3ncom  17895  psgnunilem3  17916  frgp0  18173  cmn32  18211  cmn12  18213  abladdsub  18220  ablsubsub23  18230  mulgdi  18232  mulgsubdi  18235  dprdss  18428  dprdf1o  18431  dprdsn  18435  dmdprdsplit  18446  pgpfac1lem5  18478  srgi  18511  ringi  18560  prdsringd  18612  imasring  18619  opprring  18631  mulgass3  18637  dvrass  18690  kerf1hrm  18743  subrgunit  18798  issubrg2  18800  abvdiv  18837  lss1  18939  lsssn0  18948  islss3  18959  prdslmodd  18969  islmhm2  19038  lspsolv  19143  lbsextlem4  19161  sralmod  19187  issubassa  19324  sraassa  19325  psrbaglesupp  19368  psrbagcon  19371  psrgrp  19398  psrlmod  19401  psrring  19411  psrassa  19414  mpllsslem  19435  ipdi  19985  ipsubdir  19987  ipsubdi  19988  ipassr  19991  ipassr2  19992  isphld  19999  ocvlss  20016  mamudm  20194  matring  20249  matassa  20250  ofco2  20257  scmatlss  20331  ma1repveval  20377  mdetunilem1  20418  mdetunilem9  20426  monmatcollpw  20584  iinopn  20707  restopnb  20979  subbascn  21058  nrmsep2  21160  isnrm3  21163  t1sep  21174  regsep2  21180  dnsconst  21182  dfconn2  21222  dislly  21300  tx1stc  21453  qtophmeo  21620  filss  21657  infil  21667  fsubbas  21671  filssufilg  21715  hauspwpwf1  21791  cnextcn  21871  tmdcn2  21893  psmettri  22116  isxmet2d  22132  xmettri  22156  xmetres2  22166  bldisj  22203  blss2ps  22208  blss2  22209  xmstri2  22271  mstri2  22272  xmstri  22273  mstri  22274  xmstri3  22275  mstri3  22276  msrtri  22277  comet  22318  met2ndci  22327  ngprcan  22414  ngplcan  22415  ngpsubcan  22418  nmtri2  22431  nrgdsdi  22469  nrgdsdir  22470  nlmdsdi  22485  nlmdsdir  22486  blcvx  22601  iocopnst  22739  icccvx  22749  pi1grplem  22849  pi1xfrf  22853  pi1cof  22859  clmpm1dir  22903  cmodscmulexp  22922  cvsdiv  22932  cvsdivcl  22933  cphdivcl  22982  cphsubdir  23008  cphsubdi  23009  bcthlem5  23125  rrxcph  23180  volfiniun  23315  volcn  23374  itg1val2  23451  dvconst  23680  dvlip  23756  ftc1a  23800  ulmdvlem3  24156  ang180  24544  cvxcl  24711  scvxcvx  24712  sgmmul  24926  logexprlim  24950  dchrabl  24979  motgrp  25438  iscgra1  25702  cgrane2  25705  cgrane4  25707  cgrahl1  25708  cgrahl2  25709  cgracgr  25710  cgratr  25715  cgrabtwn  25717  cgrahl  25718  dfcgra2  25721  sacgr  25722  f1otrge  25752  xmstrkgc  25766  colinearalglem1  25786  colinearalg  25790  axcgrtr  25795  axlowdimlem16  25837  axeuclidlem  25842  axcontlem4  25847  axcontlem7  25850  axcontlem12  25855  eengtrkg  25865  eengtrkge  25866  edglnl  26038  subgruhgredgd  26176  upgrwlkdvde  26633  crctcshwlkn0lem5  26706  crctcshwlkn0  26713  umgrwwlks2on  26850  rusgrnumwwlks  26869  rusgrnumwlkg  26872  3spthd  27036  frgr2wwlkeqm  27195  numclwwlk5  27246  friendship  27257  grpomuldivass  27395  ablodivdiv4  27408  ablonnncan  27410  dipdi  27698  dipsubdi  27704  disjdsct  29480  omndmul2  29712  archiabllem2c  29749  dvrdir  29790  dvrcan5  29793  reofld  29840  pstmfval  29939  qqhval2lem  30025  qqhvq  30031  esumcvg  30148  sigaclcu  30180  measdivcstOLD  30287  measdivcst  30288  carsggect  30380  tgoldbachgtd  30740  bnj970  31017  bnj910  31018  erdszelem9  31181  cvmseu  31258  elmrsubrn  31417  noprefixmo  31848  nosupbnd1  31860  ssltsep  31905  cgrid2  32110  btwncomim  32120  btwnswapid  32124  trisegint  32135  cgrxfr  32162  btwnxfr  32163  brofs2  32184  brifs2  32185  endofsegid  32192  btwnconn1lem11  32204  btwnconn2  32209  segcon2  32212  seglemin  32220  segletr  32221  btwnsegle  32224  colinbtwnle  32225  broutsideof2  32229  btwnoutside  32232  broutsideof3  32233  outsideoftr  32236  outsidele  32239  ellines  32259  linethrueu  32263  unbdqndv2  32502  poimirlem28  33437  ftc1anc  33493  sdclem1  33539  sstotbnd2  33573  ismndo1  33672  zerdivemp1x  33746  isdrngo2  33757  iscringd  33797  lsmsat  34295  lfladdcl  34358  lflnegcl  34362  lflvscl  34364  lshpkrlem4  34400  lshpkrlem6  34402  ldualgrplem  34432  lduallmodlem  34439  latmassOLD  34516  latm12  34517  latm32  34518  latmrot  34519  latmmdiN  34521  latmmdir  34522  omlfh1N  34545  omlfh3N  34546  cvrnbtwn2  34562  cvlexchb1  34617  cvlexch3  34619  cvlexch4N  34620  cvlatexchb1  34621  cvlsupr2  34630  hlatjass  34656  hlatj12  34657  hlatj32  34658  cvrat  34708  atcvrj0  34714  cvrat2  34715  atltcvr  34721  atexchltN  34727  cvrat3  34728  cvrat4  34729  atbtwnexOLDN  34733  atbtwnex  34734  3dimlem3  34747  3dimlem3OLDN  34748  3at  34776  2atneat  34801  llncmp  34808  2at0mat0  34811  2atmat0  34812  islpln2a  34834  llncvrlpln  34844  lplncmp  34848  3atnelvolN  34872  4atlem11  34895  lplncvrlvol  34902  lvolcmp  34903  2atm2atN  35071  elpaddatriN  35089  elpadd2at2  35093  paddasslem8  35113  paddasslem17  35122  paddass  35124  padd12N  35125  paddssw1  35129  pmodlem2  35133  pmodN  35136  pmapjlln1  35141  atmod1i2  35145  pexmidlem2N  35257  pexmidlem7N  35262  pl42lem2N  35266  pl42lem3N  35267  pl42lem4N  35268  pl42N  35269  lhp2lt  35287  lhpm0atN  35315  lautlt  35377  lautcvr  35378  lautj  35379  lautm  35380  ltrneq2  35434  cdleme1b  35513  cdleme3b  35516  cdleme3c  35517  cdleme9b  35539  cdlemefs27cl  35701  cdleme42mN  35775  cdlemg4c  35900  trljco  36028  tgrpgrplem  36037  tendoplass  36071  tendodi1  36072  tendodi2  36073  erngplus2  36092  erngplus2-rN  36100  cdlemk36  36201  erngdvlem3  36278  erngdvlem3-rN  36286  dvaplusgv  36298  tendospass  36308  tendospdi1  36309  dvalveclem  36314  dialss  36335  dvhvaddass  36386  dvhopvsca  36391  dvhlveclem  36397  diblss  36459  diclss  36482  diclspsn  36483  cdlemn11pre  36499  dihmeetlem12N  36607  dihmeetlem16N  36611  dihmeetlem17N  36612  dvh4dimN  36736  lpolsatN  36777  lpolpolsatN  36778  dochpolN  36779  lclkr  36822  lclkrs  36828  lcfr  36874  irrapxlem6  37391  jm2.26lem3  37568  mpaamn  37726  mendring  37762  mendlmod  37763  mendassa  37764  neicvgel1  38417  rfcnpre4  39193  fmuldfeq  39815  stoweidlem43  40260  stoweidlem52  40269  stoweidlem53  40270  stoweidlem56  40273  issmfgt  40965  issmfge  40978  iccelpart  41369  pfxccat3a  41429  fmtnoprmfac1  41477  fmtnoprmfac2  41479  copissgrp  41808  ringrng  41879  cznrng  41955  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  linccl  42203  lincsumscmcl  42222  ldepsprlem  42261  lincresunit3lem1  42268