Theorem simpl1 960

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

Assertion

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

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 957	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	adantr 452	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936

This theorem is referenced by:  simpll1  996  simprl1  1002  simp1l1  1050  simp2l1  1056  simp3l1  1062  3anandirs  1286  rspc3ev  3022  brcogw  5000  cocan1  5983  weniso  6034  smogt  6588  smorndom  6589  omeulem1  6784  nnmord  6834  nnmword  6835  difsnen  7149  mapunen  7235  ac6sfi  7310  fipreima  7370  elfiun  7393  ordiso2  7440  wemaplem2  7472  wemapso  7476  en2eqpr  7847  indcardi  7878  fodomfi2  7897  iunfictbso  7951  infmap2  8054  cofsmo  8105  cfsmolem  8106  coftr  8109  fin23lem11  8153  fincssdom  8159  fin23lem26  8161  isf32lem9  8197  ac6num  8315  gchdomtri  8460  gchpwdom  8505  winainflem  8524  tskuni  8614  gruima  8633  gruf  8642  grudomon  8648  elnpi  8821  distrlem4pr  8859  prlem934  8866  addcan  9206  addcan2  9207  ltmul1a  9815  ledivmulOLD  9840  ledivmul2OLD  9844  suprleub  9928  supmul1  9929  infmrgelb  9944  suprzcl  10305  uzsupss  10524  xleadd1a  10788  xlesubadd  10798  xmulasslem3  10821  xlemul2a  10824  xadddilem  10829  xadddi2  10832  ixxun  10888  icoshftf1o  10976  lincmb01cmp  10994  iccf1o  10995  ltexp2a  11386  leexp2  11389  ltexp2r  11391  exple1  11394  expnlbnd2  11465  ccatass  11705  ccatopth  11731  s2f1o  11818  limsupgre  12230  addcn2  12342  mulcn2  12344  dvdsadd2b  12847  dvdsmod  12861  oexpneg  12866  gcdass  13000  rplpwr  13011  rppwr  13012  coprmdvds2  13058  rpmulgcd2  13060  qredeq  13061  rpexp  13075  rpdvds  13079  prmdiveq  13130  odzdvds  13136  coprimeprodsq2  13139  pythagtriplem3  13147  pcdvdsb  13197  pcgcd1  13205  qexpz  13225  pockthg  13229  vdwnnlem1  13318  0ram  13343  ramz2  13347  lubss  14503  lubun  14505  clatleglb  14508  clatglbss  14509  mrelatglb  14565  issubmnd  14679  gsumccat  14742  frmdss2  14763  mulgneg  14863  mulgdirlem  14869  submmulg  14880  subgmulg  14913  nmzsubg  14936  ghmmulg  14973  odmodnn0  15133  odnncl  15138  odmod  15139  odmulgid  15145  odmulgeq  15148  odf1o1  15161  odf1o2  15162  odngen  15166  gexdvdsi  15172  pgpfi1  15184  odcau  15193  subgslw  15205  fislw  15214  lsmssv  15232  lsmless1x  15233  lsmless2x  15234  lsmsubm  15242  lsmmod  15262  lsmmod2  15263  efgred  15335  cntzcmn  15414  ghmplusg  15416  odadd1  15418  odadd2  15419  odadd  15420  lsmcomx  15426  gsumconst  15487  rng1eq0  15657  mulgass2  15665  isabvd  15863  lssintcl  15995  0lmhm  16071  lmhmvsca  16076  reslmhm2b  16085  lspfixed  16155  lspsnat  16172  lidldvgen  16281  issubassa  16338  psrplusgpropd  16584  coe1subfv  16614  coe1mul2  16617  xrsdsreclblem  16699  obselocv  16910  riinopn  16936  neiint  17123  topssnei  17143  restntr  17200  iscnp4  17281  cnconst2  17301  cnrest2  17304  cnprest2  17308  cnpdis  17311  cnt0  17364  cnt1  17368  cnhaus  17372  ordthauslem  17401  cncmp  17409  fiuncmp  17421  sscmp  17422  hauscmp  17424  cnconn  17438  uncon  17445  nlly2i  17492  llynlly  17493  nllyidm  17505  ptrescn  17624  xkococnlem  17644  qtoptop2  17684  qtopss  17700  kqfvima  17715  r0cld  17723  ordthmeolem  17786  fbssint  17823  fmf  17930  fmss  17931  elfm  17932  rnelfmlem  17937  rnelfm  17938  fmco  17946  flimss2  17957  flimss1  17958  flimrest  17968  flftg  17981  cnpflf2  17985  cnpflf  17986  flfcnp  17989  supnfcls  18005  fclsss1  18007  fclsss2  18008  fcfnei  18020  fcfelbas  18021  cnpfcfi  18025  subgntr  18089  opnsubg  18090  cldsubg  18093  ghmcnp  18097  utop2nei  18233  neipcfilu  18279  bldisj  18381  blgt0  18382  bl2in  18383  blss2ps  18386  blss2  18387  blssps  18407  blss  18408  xmetresbl  18420  lpbl  18486  blcld  18488  stdbdbl  18500  metcnp3  18523  metcnp2  18525  txmetcnp  18530  blval2  18558  nmoix  18716  nmoeq0  18723  icoopnst  18917  iocopnst  18918  xrhmeo  18924  nmhmcn  19081  cphsqrcl2  19102  cphsqrcl3  19103  cfil3i  19175  caublcls  19214  bcthlem5  19234  cmetcusp1OLD  19258  cmetcusp1  19259  pjth  19293  ovoliunlem2  19352  volun  19392  volsup2  19450  mbfimaopn2  19502  iblconst  19662  itgconst  19663  dvcnp2  19759  dvcn  19760  evlsval2  19894  deg1mul3le  19992  deg1tmle  19993  dvdsq1p  20036  ig1peu  20047  ig1pdvds  20052  coeid3  20112  dgrmulc  20142  efcvx  20318  tanord  20393  logdivlti  20468  logccv  20507  recxpcl  20519  cxpeq  20594  ang180  20609  isosctrlem2  20616  cxp2lim  20768  amgm  20782  muval1  20869  dvdssqf  20874  mumullem2  20916  mumul  20917  bcmono  21014  lgsfcl2  21039  lgsdilem  21059  lgsdirprm  21066  lgsdir  21067  lgsdi  21069  lgsne0  21070  2pthon  21555  gxcom  21810  gxnn0add  21815  zerdivemp1  21975  nvmul0or  22086  ipval2lem2  22153  ipval2lem5  22159  lnomul  22214  shless  22814  shlej1  22815  pjspansn  23032  hoadddi  23259  kbmul  23411  homco2  23433  kbass2  23573  snunioc  24090  eliccelico  24093  elicoelioo  24094  iocinioc2  24095  iocinif  24097  ress0g  24135  xrge0adddir  24168  xrge0npcan  24169  rhmdvdsr  24209  pstmfval  24244  fmcncfil  24270  zrhnm  24306  qqhnm  24327  measvunilem  24519  volfiniune  24539  dya2iocnrect  24584  probun  24630  probinc  24632  cndprob01  24646  pconpi1  24877  cvmsss2  24914  ntrivcvgmul  25183  binomrisefac  25309  dvdspw  25317  br6  25328  br4  25329  frrlem4  25498  brbtwn2  25748  colinearalglem1  25749  colinearalg  25753  axcgrtr  25758  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  axcontlem8  25814  axcontlem10  25816  cgrcomim  25827  cgrtriv  25840  cgrextend  25846  segconeq  25848  btwntriv2  25850  btwnintr  25857  btwnexch3  25858  btwnouttr2  25860  trisegint  25866  cgrsub  25883  cgrxfr  25893  btwnxfr  25894  lineext  25914  btwnconn1lem13  25937  btwnconn1lem14  25938  btwnconn3  25941  segcon2  25943  brsegle  25946  brsegle2  25947  segletr  25952  segleantisym  25953  seglelin  25954  outsideofeu  25969  lineunray  25985  lineelsb2  25986  areacirc  26187  ivthALT  26228  finlocfin  26269  cocanfo  26309  upixp  26321  ismtyima  26402  rrndstprj2  26430  zerdivemp1x  26461  mzprename  26696  eldioph2lem1  26708  lzunuz  26716  rencldnfi  26772  pellexlem2  26783  infmrgelbi  26831  pellfundglb  26838  pellfund14gap  26840  qirropth  26861  rmxycomplete  26870  congadd  26921  acongeq  26938  jm2.19  26954  jm2.23  26957  jm2.20nn  26958  jm2.27  26969  jm3.1  26981  aomclem6  27024  lnmepi  27051  lmhmfgsplit  27052  lmhmlnmsplit  27053  pwssplit1  27056  pwssplit3  27058  pwssplit4  27059  uvcresum  27110  frlmsslsp  27116  frlmup4  27121  enfixsn  27125  lindff1  27158  f1lindf  27160  lsslindf  27168  islindf4  27176  lbslcic  27179  hbtlem2  27196  hbtlem5  27200  dgraa0p  27222  pmtrfb  27274  psgnunilem4  27288  mhmvlin  27320  hashgcdlem  27384  proot1hash  27387  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem28  27644  stoweidlem34  27650  stoweidlem44  27660  stoweidlem60  27676  wallispilem3  27683  swrd0swrd  28009  swrdswrdlem  28010  bnj517  28962  bnj594  28989  lubunNEW  29456  lsatfixedN  29492  lssat  29499  eqlkr  29582  eqlkr2  29583  lkrlsp  29585  lshpkrlem4  29596  opposet  29665  cvrcon3b  29760  cvrcmp  29766  atlen0  29793  atnle  29800  atlatmstc  29802  cvlatexch3  29821  cvlsupr2  29826  hlsupr2  29869  hlrelat2  29885  cvrexchlem  29901  lnnat  29909  atcvrj2b  29914  atle  29918  atexchcvrN  29922  atbtwn  29928  athgt  29938  3dimlem3  29943  3dim1  29949  1cvratlt  29956  1cvrjat  29957  ps-1  29959  ps-2  29960  3atlem3  29967  3atlem5  29969  3atlem7  29971  llni  29990  llni2  29994  atcvrlln2  30001  llnexatN  30003  llncmp  30004  2llnmat  30006  2at0mat0  30007  lplni  30014  lplnnle2at  30023  2atnelpln  30026  lplnllnneN  30038  llncvrlpln2  30039  2lplnmN  30041  2llnmj  30042  lplncmp  30044  lplnexatN  30045  lplnexllnN  30046  2llnm3N  30051  lvoli  30057  lvoli3  30059  islvol2aN  30074  4atlem0a  30075  4atlem3  30078  4atlem3a  30079  4atlem4a  30081  4atlem4b  30082  4atlem4c  30083  4atlem4d  30084  4atlem10b  30087  4atlem11  30091  4atlem12  30094  lplncvrlvol2  30097  lvolcmp  30099  2lplnmj  30104  islinei  30222  pmapglbx  30251  linepmap  30257  lneq2at  30260  lnjatN  30262  lncvrat  30264  lncmp  30265  2llnma3r  30270  elpaddatriN  30285  elpaddat  30286  paddcom  30295  paddss1  30299  paddss2  30300  paddss12  30301  paddasslem6  30307  paddasslem7  30308  paddasslem8  30309  paddasslem9  30310  paddasslem15  30316  pmodlem2  30329  pmodl42N  30333  pmapjoin  30334  llnmod1i2  30342  2polcon4bN  30400  polcon2bN  30402  poml4N  30435  poml6N  30437  osumcllem1N  30438  osumcllem2N  30439  osumcllem11N  30448  osumclN  30449  pmapojoinN  30450  pexmidlem2N  30453  pexmidlem3N  30454  pexmidlem4N  30455  pexmidlem6N  30457  pexmidlem7N  30458  pl42lem2N  30462  pl42lem3N  30463  pl42lem4N  30464  pl42N  30465  lhpexle2lem  30491  lhpexle3lem  30493  lhpexle3  30494  lhpmcvr3  30507  lhp2at0nle  30517  lhprelat3N  30522  4atex  30558  4atex2  30559  lauteq  30577  lautco  30579  ltrncoidN  30610  ltrneq2  30630  ltrnnidn  30656  ltrnideq  30657  trlnid  30661  ltrnatlw  30665  trlnle  30668  trlval3  30669  trlval4  30670  cdlemc  30679  cdlemd5  30684  cdlemd9  30688  ltrneq3  30690  cdleme0moN  30707  cdleme20  30806  cdleme21j  30818  cdleme21  30819  cdleme27cl  30848  cdlemefrs29bpre0  30878  cdlemefs27cl  30895  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme32d  30926  cdleme32f  30928  cdleme32le  30929  cdleme35h2  30939  cdleme38n  30946  cdleme40m  30949  cdleme41snaw  30958  cdleme42ke  30967  cdleme17d3  30978  cdleme48fvg  30982  cdlemeg46fvcl  30988  cdlemeg46fgN  31016  cdleme48gfv1  31018  cdleme48fgv  31020  cdleme50trn3  31035  trlord  31051  ltrniotavalbN  31066  cdlemb3  31088  cdlemg6c  31102  cdlemg6  31105  cdlemg7N  31108  cdlemg8c  31111  cdlemg8  31113  cdlemg11a  31119  cdlemg11b  31124  cdlemg12e  31129  cdlemg15a  31137  cdlemg15  31138  cdlemg16  31139  cdlemg16z  31141  cdlemg16zz  31142  cdlemg17dN  31145  cdlemg18a  31160  cdlemg20  31167  cdlemg22  31169  cdlemg24  31170  cdlemg37  31171  cdlemg31d  31182  cdlemg29  31187  cdlemg33b  31189  cdlemg33  31193  cdlemg38  31197  cdlemg39  31198  cdlemg40  31199  trlco  31209  trlcone  31210  cdlemg42  31211  cdlemg44b  31214  ltrncom  31220  trljco  31222  tendococl  31254  tendoplcl  31263  tendoplcom  31264  cdlemj2  31304  cdlemj3  31305  tendoid0  31307  tendoconid  31311  tendotr  31312  cdlemk25-3  31386  cdlemk26b-3  31387  cdlemk34  31392  cdlemk36  31395  cdlemk38  31397  cdlemkid4  31416  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk19x  31425  cdlemk53  31439  cdlemk55  31443  cdlemk55u  31448  cdlemk39u  31450  cdlemk19u  31452  cdlemk56  31453  tendoex  31457  cdleml3N  31460  cdleml5N  31462  tendospcanN  31506  cdlemm10N  31601  cdlemn11pre  31693  dihord2pre  31708  dihvalcqpre  31718  dihopelvalcpre  31731  dihord6apre  31739  dihord5b  31742  dihord5apre  31745  dihord  31747  dihmeetlem1N  31773  dihglblem5apreN  31774  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetbN  31786  dihmeetlem4preN  31789  dihmeetlem5  31791  dihmeetlem7N  31793  dihmeetlem10N  31799  dihmeetlem11N  31800  dihmeetlem12N  31801  dihmeetlem13N  31802  dihmeetlem15N  31804  dihmeetlem16N  31805  dihmeetlem17N  31806  dihmeetlem18N  31807  dihmeetlem19N  31808  dihmeetALTN  31810  dih1dimatlem0  31811  dihlspsnssN  31815  dihlspsnat  31816  mapdh8ad  32262  hdmap14lem14  32367  hgmapvvlem3  32411

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

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938