Theorem simpl2 1065

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

Assertion

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

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simp2 1062	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
2	1	adantr 481	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )

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:  simpll2  1101  simprl2  1107  simp1l2  1155  simp2l2  1161  simp3l2  1167  3anandirs  1435  rspc3ev  3326  f1prex  6539  weniso  6604  ofmpteq  6916  tfisi  7058  mpt2sn  7268  smogt  7464  smorndom  7465  omeulem1  7662  nnmord  7712  nnmword  7713  difsnen  8042  enfixsn  8069  mapunen  8129  ac6sfi  8204  ordiso2  8420  wemaplem2  8452  wemapso  8456  wemapso2lem  8457  en2eqpr  8830  acndom  8874  infmap2  9040  cflim2  9085  cfsmolem  9092  coftr  9095  fin23lem26  9147  isf32lem9  9183  fin1a2lem9  9230  fin1a2lem10  9231  ac6num  9301  gchdomtri  9451  canth4  9469  gchpwdom  9492  gruima  9624  grudomon  9639  prn0  9811  distrlem4pr  9848  prlem934  9855  addcan  10220  addcan2  10221  divmulass  10708  divmulasscom  10709  ltmul1a  10872  supmul1  10992  uzsupss  11780  xaddass  12079  xleadd1a  12083  xlesubadd  12093  xmulass  12117  xlemul2a  12119  xadddilem  12124  xadddi  12125  ixxdisj  12190  ixxun  12191  ixxlb  12197  icoshftf1o  12295  icodisj  12297  lincmb01cmp  12315  iccf1o  12316  elfz1b  12409  ssfzoulel  12562  modmuladd  12712  modaddmulmod  12737  ltexp2a  12912  leexp2  12915  ltexp2r  12917  exple1  12920  expnlbnd2  12995  mulsubdivbinom2  13046  fun2dmnop0  13276  ccatass  13371  ccatopth  13470  swrdccatin12lem2a  13485  repswccat  13532  cshwidxmodr  13550  2cshw  13559  repsco  13585  s2f1o  13661  limsupgle  14208  limsupgre  14212  addcn2  14324  mulcn2  14326  binomrisefac  14773  dvdsval2  14986  dvdsadd2b  15028  dvdsmod  15050  oexpneg  15069  sadass  15193  gcdass  15264  rplpwr  15276  rppwr  15277  lcmass  15327  coprmdvds2  15368  rpmulgcd2  15370  rpdvds  15374  coprmprod  15375  cncongr2  15382  rpexp  15432  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  coprimeprodsq2  15514  pythagtriplem3  15523  pythagtriplem4  15524  pcdvdsb  15573  vdwnnlem1  15699  0ram  15724  ramz2  15728  ramub1lem1  15730  mremre  16264  mrieqv2d  16299  lubss  17121  lubun  17123  clatleglb  17126  clatglbss  17127  mrelatglb  17184  isnsgrp  17288  issubmnd  17318  gsumccat  17378  frmdss2  17400  nmzsubg  17635  ghmnsgima  17684  gsmsymgreqlem1  17850  psgnunilem4  17917  odmodnn0  17959  odnncl  17964  odmod  17965  oddvds  17966  odeq  17969  odmulgid  17971  odmulgeq  17974  odbezout  17975  odf1o1  17987  odf1o2  17988  odngen  17992  gexdvdsi  17998  pgpfi1  18010  odcau  18019  subgslw  18031  fislw  18040  lsmless1x  18059  lsmless2x  18060  lsmsubm  18068  lsmmod  18088  lsmmod2  18089  efgsfo  18152  odadd1  18251  odadd2  18252  odadd  18253  lsmcomx  18259  prdscmnd  18264  gsumconst  18334  srg1zr  18529  csrgbinom  18546  ring1eq0  18590  mulgass2  18601  cntzsubr  18812  isabvd  18820  rmodislmod  18931  0lmhm  19040  lmhmvsca  19045  reslmhm2b  19054  pwssplit1  19059  pwssplit2  19060  pwssplit3  19061  lbspss  19082  lspsnat  19145  lidldvgen  19255  issubassa  19324  evlsval2  19520  coe1subfv  19636  coe1sclmul  19652  coe1sclmul2  19654  xrsdsreclblem  19792  cssmre  20037  obs2ss  20073  uvcresum  20132  frlmsslsp  20135  frlmup4  20140  lindff1  20159  f1lindf  20161  lsslindf  20169  islindf4  20177  mpt2matmul  20252  mamutpos  20264  scmatscmide  20313  mavmulsolcl  20357  mulmarep1gsum2  20380  mdetdiaglem  20404  mdetdiag  20405  mdetunilem1  20418  mdetunilem3  20420  mdetunilem9  20426  maducoeval2  20446  madurid  20450  slesolinvbi  20487  cramerimplem1  20489  cramerlem1  20493  cramer  20497  cpmatel2  20518  m2cpm  20546  m2pmfzmap  20552  m2cpminvid2lem  20559  m2cpminvid2  20560  decpmatmul  20577  pmatcollpw1lem2  20580  pmatcollpw1  20581  pmatcollpw2lem  20582  pmatcollpwfi  20587  pm2mpcl  20602  mply1topmatcl  20610  mp2pm2mplem2  20612  mp2pm2mplem4  20614  mp2pm2mplem5  20615  mp2pm2mp  20616  pm2mpghmlem2  20617  pm2mpghmlem1  20618  chfacfisfcpmat  20660  topssnei  20928  cnconst2  21087  cnpresti  21092  cnprest2  21094  cnpdis  21097  cnt0  21150  cnt1  21154  cnhaus  21158  sscmp  21208  hauscmp  21210  cnconn  21225  unconn  21232  finlocfin  21323  comppfsc  21335  kgen2ss  21358  ptpjopn  21415  prdstopn  21431  ptrescn  21442  qtopss  21518  kqfvima  21533  fbssint  21642  fbasrn  21688  filuni  21689  fmss  21750  rnelfm  21757  fmufil  21763  fmco  21765  flimss2  21776  flimss1  21777  flimrest  21787  cnpflf2  21804  flfcnp  21808  supnfcls  21824  fclsss1  21826  fclsss2  21827  isfcf  21838  subgntr  21910  opnsubg  21911  cldsubg  21914  ghmcnp  21918  ustuqtop1  22045  bldisj  22203  blgt0  22204  bl2in  22205  blss2ps  22208  blss2  22209  blssps  22229  blss  22230  xmetresbl  22242  lpbl  22308  blcld  22310  stdbdmopn  22323  metcnp3  22345  metcnp  22346  metcnp2  22347  txmetcnp  22352  blval2  22367  nmoix  22533  nmoi2  22534  nmotri  22543  metdsge  22652  metdseq0  22657  iocopnst  22739  xrhmeo  22745  nmhmcn  22920  cphsqrtcl2  22986  cphsqrtcl3  22987  pjth  23210  ovoliunlem2  23271  volun  23313  mbfimaopn2  23424  iblconst  23584  limcvallem  23635  dvfval  23661  dvcnp2  23683  dvcn  23684  deg1mul3le  23876  deg1tmle  23877  dvdsq1p  23920  ig1peu  23931  ig1pdvds  23936  ply1term  23960  coeid3  23996  dgrmulc  24027  dvply1  24039  aaliou2  24095  efcvx  24203  tanord  24284  eflogeq  24348  logdivlti  24366  logccv  24409  recxpcl  24421  cxplea  24442  cxpeq  24498  ang180  24544  isosctrlem2  24549  cxp2lim  24703  amgm  24717  muval1  24859  dvdssqf  24864  mumullem2  24906  mumul  24907  bcmono  25002  lgsneg  25046  lgsdilem  25049  lgsdirprm  25056  lgsdir  25057  lgsdi  25059  lgsne0  25060  brbtwn2  25785  colinearalglem1  25786  colinearalg  25790  axcgrtr  25795  axsegconlem8  25804  axsegconlem9  25805  axsegconlem10  25806  axcontlem2  25845  axcontlem10  25853  ewlkle  26501  edginwlkOLD  26531  crctcshwlkn0lem5  26706  wwlknp  26734  wwlksnext  26788  wspthsnwspthsnon  26811  clwlkclwwlklem3  26902  erclwwlkssym  26935  erclwwlksnsym  26947  upgriseupth  27067  eucrct2eupth  27105  3cyclfrgrrn  27150  numclwwlkovf2exlem2  27212  frgrregord13  27254  nvmul0or  27505  ipval2lem2  27559  lnoadd  27613  lnosub  27614  lnomul  27615  shless  28218  shlej1  28219  kbmul  28814  homco2  28836  kbass2  28976  eliccelico  29539  elicoelioo  29540  iocinioc2  29541  iocinif  29543  difioo  29544  xrge0adddir  29692  xrge0npcan  29694  isarchi2  29739  archiabl  29752  rhmdvdsr  29818  pstmfval  29939  fmcncfil  29977  zrhnm  30013  qqhnm  30034  nexple  30071  volfiniune  30293  dya2iocnrect  30343  probinc  30483  cndprob01  30497  signswmnd  30634  bnj517  30955  cvmsss2  31256  cvmlift2lem10  31294  br6  31647  funsseq  31666  frrlem4  31783  nolesgn2o  31824  nosep1o  31832  nosepssdm  31836  nosupres  31853  nosupbnd1lem1  31854  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  noetalem2  31864  cgrtriv  32109  5segofs  32113  btwnouttr2  32129  btwnxfr  32163  lineext  32183  btwnconn1lem13  32206  brsegle2  32216  nn0prpwlem  32317  lindsenlbs  33404  blbnd  33586  ismtyima  33602  rrndstprj2  33630  ghomdiv  33691  grpokerinj  33692  lsatfixedN  34296  lssat  34303  lshpkrlem4  34400  cvrcon3b  34564  atlen0  34597  atcvreq0  34601  atnle  34604  atlatmstc  34606  atlatle  34607  cvlcvr1  34626  hlsupr2  34673  hlrelat2  34689  cvrexchlem  34705  lnnat  34713  atcvrj2b  34718  3dimlem3  34747  3dim1  34753  1cvrjat  34761  llni  34794  llni2  34798  llnexatN  34807  2llnmat  34810  lplni  34818  2atnelpln  34830  llncvrlpln2  34843  2llnmj  34846  lplnexatN  34849  lplnexllnN  34850  2llnm3N  34855  lvoli  34861  lvoli3  34863  lvolnle3at  34868  islvol2aN  34878  4atlem4a  34885  4atlem4b  34886  4atlem11  34895  lplncvrlvol2  34901  2lplnmj  34908  islinei  35026  linepmap  35061  lnjatN  35066  lncvrat  35068  lncmp  35069  elpaddn0  35086  elpaddatriN  35089  elpaddat  35090  paddcom  35099  paddss2  35104  paddss12  35105  paddasslem4  35109  paddasslem9  35114  paddasslem10  35115  pmodl42N  35137  pmapjoin  35138  llnmod1i2  35146  polcon2bN  35206  pclfinclN  35236  poml4N  35239  poml6N  35241  osumcllem1N  35242  osumcllem2N  35243  osumcllem11N  35252  osumclN  35253  pmapojoinN  35254  pexmidlem2N  35257  pexmidlem3N  35258  pexmidlem4N  35259  pexmidlem6N  35261  pexmidlem7N  35262  pl42lem2N  35266  pl42lem3N  35267  pl42lem4N  35268  pl42N  35269  lhprelat3N  35326  4atex  35362  lauteq  35381  lautco  35383  ltrncoidN  35414  ltrneq2  35434  ltrnideq  35462  trlnle  35473  trlval3  35474  cdlemc  35484  cdlemd9  35493  cdlemd  35494  cdleme21j  35624  cdleme21  35625  cdleme29ex  35662  cdlemefr27cl  35691  cdlemefs27cl  35701  cdleme32d  35732  cdleme32f  35734  cdleme35h2  35745  cdleme40m  35755  cdleme17d3  35784  cdleme48fvg  35788  cdlemeg46fvcl  35794  cdlemeg46fgN  35822  cdleme48fgv  35826  cdleme50trn3  35841  cdlemb3  35894  cdlemg8  35919  cdlemg11a  35925  cdlemg15a  35943  cdlemg15  35944  cdlemg16  35945  cdlemg16z  35947  cdlemg17dN  35951  cdlemg24  35976  cdlemg37  35977  cdlemg29  35993  cdlemg33b  35995  cdlemg38  36003  cdlemg40  36005  trlco  36015  cdlemg44b  36020  ltrncom  36026  trljco  36028  tendococl  36060  tendoplcl  36069  tendoplcom  36070  cdlemj2  36110  tendoid0  36113  tendo1ne0  36116  cdlemk25-3  36192  cdlemk36  36201  cdlemkid4  36222  cdlemk19x  36231  cdlemk53  36245  cdlemk56  36259  cdleml5N  36268  tendospcanN  36312  cdlemm10N  36407  dihord6apre  36545  dihord  36553  dihmeetlem1N  36579  dihglblem2N  36583  dihmeetlem2N  36588  dihmeetbN  36592  dihmeetlem5  36597  dihmeetlem6  36598  dihmeetlem7N  36599  dihmeetlem10N  36605  dihmeetlem12N  36607  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem18N  36613  dihmeetALTN  36616  dihlspsnssN  36621  dvh3dim2  36737  dvh3dim3N  36738  lcfrlem16  36847  mapdrvallem2  36934  mapdh8ad  37068  hgmapvvlem3  37217  diophrw  37322  eldioph2lem1  37323  diophrex  37339  rencldnfi  37385  pellexlem2  37394  pellqrexplicit  37441  infmrgelbi  37442  pellfundglb  37449  pellfund14gap  37451  rmxycomplete  37482  congadd  37533  acongeq  37550  jm2.19  37560  jm2.23  37563  jm2.20nn  37564  jm2.27  37575  jm3.1  37587  lnmepi  37655  lmhmlnmsplit  37657  hbtlem2  37694  dgraa0p  37719  idomrootle  37773  proot1hash  37778  iocunico  37796  iocinico  37797  relexpxpmin  38009  ntrclsk3  38368  rfcnnnub  39195  uzwo4  39221  supxrge  39554  infleinflem2  39587  snunioo2  39731  iccintsng  39749  climsuse  39840  lptre2pt  39872  limcleqr  39876  0ellimcdiv  39881  fnlimfvre  39906  dvnprodlem1  40161  volioc  40188  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem22  40239  stoweidlem28  40245  stoweidlem34  40251  stoweidlem44  40261  stoweidlem60  40277  wallispilem3  40284  fourierdlem42  40366  fourierdlem48  40371  fourierdlem51  40374  fourierdlem54  40377  fourierdlem74  40397  fourierdlem77  40400  fourierdlem87  40410  fourierdlem97  40420  ioorrnopnlem  40524  ovnsubaddlem2  40785  smfinflem  41023  eluzge0nn0  41322  fzopredsuc  41333  fzoopth  41337  repswpfx  41436  lighneallem4  41527  oexpnegALTV  41588  oexpnegnz  41589  tgblthelfgott  41703  tgblthelfgottOLD  41709  rmsupp0  42149  rmsuppss  42151  lincresunit3lem3  42263  lincresunit3lem2  42269  lindssnlvec  42275  fdivmptf  42335  refdivmptf  42336  elbigolo1  42351