Theorem simpl3 1066

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

Assertion

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

Proof of Theorem simpl3

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

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:  simpll3  1102  simprl3  1108  simp1l3  1156  simp2l3  1162  simp3l3  1168  3anandirs  1435  f1prex  6539  fcofo  6543  soisores  6577  weniso  6604  knatar  6607  ofmpteq  6916  smorndom  7465  nnmord  7712  nnmword  7713  difsnen  8042  mapunen  8129  ac6sfi  8204  fipreima  8272  wemaplem2  8452  wemapso2lem  8457  en2eqpr  8830  indcardi  8864  acndom  8874  fodomfi2  8883  infmap2  9040  cflim2  9085  coftr  9095  infpssrlem4  9128  fin23lem11  9139  fincssdom  9145  isf32lem9  9183  fin1a2lem9  9230  gchpwdom  9492  gruima  9624  prpssnq  9812  distrlem4pr  9848  dedekind  10200  addcan  10220  addcan2  10221  divmulass  10708  supmul1  10992  uzsupss  11780  xaddass  12079  xleadd1a  12083  xlesubadd  12093  xmulasslem3  12116  xmulass  12117  xadddilem  12124  xadddi  12125  ixxun  12191  icoshftf1o  12295  snunioc  12300  difelfzle  12452  fzo1fzo0n0  12518  ssfzoulel  12562  modmuladd  12712  modifeq2int  12732  modaddmulmod  12737  modsubdir  12739  ltexp2a  12912  leexp2  12915  ltexp2r  12917  exple1  12920  expnlbnd2  12995  mulsubdivbinom2  13046  hashtpg  13267  ccatass  13371  ccatopth  13470  swrdccatin12lem2a  13485  swrdccat3  13492  cshinj  13557  s2f1o  13661  limsupgre  14212  addcn2  14324  mulcn2  14326  binomrisefac  14773  bpolydif  14786  modmulconst  15013  dvdsmod  15050  sadass  15193  gcdass  15264  rplpwr  15276  rppwr  15277  rpmulgcd2  15370  rpdvds  15374  rpexp  15432  prmdiveq  15491  hashgcdlem  15493  coprimeprodsq  15513  coprimeprodsq2  15514  pythagtriplem3  15523  pcdvdsb  15573  pcgcd1  15581  dvdsprmpweq  15588  pcbc  15604  0ram  15724  ramz2  15728  ramub1lem1  15730  setsstructOLD  15899  mremre  16264  mrieqv2d  16299  lubun  17123  isnsgrp  17288  issubmnd  17318  gsumccat  17378  frmdss2  17400  sgrp2rid2ex  17414  mulgnn0p1  17552  mulgnnsubcl  17553  mulgneg  17560  mulgdirlem  17572  nmzsubg  17635  ghmmulg  17672  pmtrfv  17872  pmtrmvd  17876  pmtrfb  17885  odmodnn0  17959  oddvdsnn0  17963  odnncl  17964  odmod  17965  oddvds  17966  odeq  17969  odmulgid  17971  odmulg  17973  odmulgeq  17974  odbezout  17975  odf1o1  17987  odf1o2  17988  odngen  17992  odcau  18019  pgpssslw  18029  fislw  18040  lsmless1x  18059  lsmless2x  18060  lsmsubm  18068  lsmmod  18088  lsmmod2  18089  efgsfo  18152  cntzcmn  18245  odadd1  18251  odadd2  18252  odadd  18253  lsmcomx  18259  prdscmnd  18264  gsumconst  18334  ring1eq0  18590  cntzsubr  18812  isabvd  18820  rmodislmod  18931  lspss  18984  0lmhm  19040  reslmhm2  19053  pwssplit0  19058  pwssplit1  19059  lbspss  19082  lspfixed  19128  lsmcv  19141  lspsnat  19145  issubassa  19324  aspss  19332  coe1subfv  19636  coe1tm  19643  xrsdsreclblem  19792  obselocv  20072  frlmsplit2  20112  frlmsslss2  20114  frlmup4  20140  lindff1  20159  lsslindf  20169  lsslinds  20170  islindf4  20177  mpt2matmul  20252  mamutpos  20264  submaval  20387  mdetdiag  20405  mdetunilem1  20418  mdetunilem3  20420  mdetunilem9  20426  mdetmul  20429  maducoeval2  20446  madurid  20450  minmar1val  20454  cramer  20497  cpmatel2  20518  m2cpm  20546  decpmatmul  20577  pmatcollpw1lem2  20580  pmatcollpw1  20581  pmatcollpw2lem  20582  pm2mpcl  20602  mply1topmatcl  20610  mp2pm2mplem2  20612  mp2pm2mplem4  20614  pm2mpghmlem2  20617  pm2mpghmlem1  20618  cayhamlem2  20689  neiint  20908  topssnei  20928  cnrest2  21090  cnprest2  21094  cnt0  21150  cnt1  21154  cnhaus  21158  cncmp  21195  fiuncmp  21207  sscmp  21208  hauscmp  21210  cnconn  21225  unconn  21232  comppfsc  21335  kgen2ss  21358  ptpjopn  21415  ptrescn  21442  qtopss  21518  kqfvima  21533  r0cld  21541  cmphaushmeo  21603  fbssint  21642  fbasrn  21688  filuni  21689  ufilmax  21711  fin1aufil  21736  fmf  21749  fmss  21750  rnelfmlem  21756  rnelfm  21757  fmufil  21763  fmco  21765  flimss2  21776  flimss1  21777  flimrest  21787  cnpflf2  21804  cnpflf  21805  flfcnp  21808  lmflf  21809  supnfcls  21824  fclsss1  21826  fclsss2  21827  cnpfcfi  21844  subgntr  21910  opnsubg  21911  cldsubg  21914  ustuqtop1  22045  ucncn  22089  bldisj  22203  blgt0  22204  bl2in  22205  blss2ps  22208  blss2  22209  xbln0  22219  blssps  22229  blss  22230  lpbl  22308  blcld  22310  blcls  22311  stdbdmopn  22323  metcnp2  22347  txmetcnp  22352  blval2  22367  restmetu  22375  nmoix  22533  nmoi2  22534  nmoeq0  22540  nmotri  22543  metdsge  22652  metds0  22653  metdseq0  22657  icoopnst  22738  iccpnfhmeo  22744  xrhmeo  22745  nmhmcn  22920  cphsqrtcl2  22986  cphsqrtcl3  22987  fmcfil  23070  bcthlem5  23125  cmetcusp1  23149  pjth  23210  ovolunnul  23268  volun  23313  voliunlem2  23319  itg2const  23507  iblconst  23584  itgconst  23585  limcvallem  23635  dvcnp2  23683  dvcn  23684  deg1mul3le  23876  deg1tmle  23877  ig1pdvds  23936  coe11  24009  dgrmulc  24027  dvply1  24039  aaliou2  24095  efcvx  24203  tanord  24284  logdivlti  24366  logccv  24409  recxpcl  24421  cxplea  24442  cxple2a  24445  ang180  24544  isosctrlem2  24549  cxp2lim  24703  amgm  24717  muval1  24859  dvdssqf  24864  mumullem2  24906  bcmono  25002  lgsneg  25046  lgsmod  25048  lgsdirprm  25056  lgsdir  25057  lgsdi  25059  brbtwn2  25785  colinearalglem1  25786  colinearalg  25790  axcgrtr  25795  axcontlem2  25845  upgrewlkle2  26502  wlksoneq1eq2  26560  crctcshwlkn0lem5  26706  wspthsnwspthsnon  26811  lppthon  27011  upgriseupth  27067  4cyclusnfrgr  27156  numclwwlk5  27246  nvmul0or  27505  shless  28218  shlej1  28219  pjspansn  28436  kbmul  28814  homco2  28836  kbass2  28976  padct  29497  eliccelico  29539  elicoelioo  29540  iocinioc2  29541  difioo  29544  xrge0npcan  29694  isarchi2  29739  archiabl  29752  mdetlap1  29892  pstmfval  29939  fmcncfil  29977  zrhnm  30013  qqhnm  30034  nexple  30071  volfiniune  30293  omsmeas  30385  eulerpartlemb  30430  probinc  30483  cndprob01  30497  signswmnd  30634  cvmsss2  31256  dvdspw  31636  funsseq  31666  sltres  31815  nolt02olem  31844  nolt02o  31845  nosupbnd1lem1  31854  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  cgrtriv  32109  5segofs  32113  btwntriv2  32119  btwnxfr  32163  segcon2  32212  brsegle2  32216  seglelin  32223  outsideofeu  32238  lindsenlbs  33404  mblfinlem2  33447  blbnd  33586  rrndstprj2  33630  zerdivemp1x  33746  lsmsat  34295  lsatfixedN  34296  lssat  34303  lkrlsp  34389  lshpkrlem4  34400  cvrcon3b  34564  leat3  34582  atlen0  34597  atnle  34604  atlatmstc  34606  atlatle  34607  cvlcvr1  34626  cvlsupr2  34630  hlsupr2  34673  hlrelat2  34689  cvrexchlem  34705  cvratlem  34707  lnnat  34713  atexchcvrN  34726  1cvratlt  34760  1cvrjat  34761  3atlem3  34771  3atlem7  34775  llni2  34798  atcvrlln2  34805  llnexatN  34807  llncmp  34808  2llnmat  34810  2at0mat0  34811  2atnelpln  34830  llncvrlpln2  34843  2lplnmN  34845  2llnmj  34846  lplncmp  34848  lplnexatN  34849  2llnjaN  34852  lvoli3  34863  islvol2aN  34878  4atlem3a  34883  4atlem4a  34885  4atlem4b  34886  4atlem11  34895  4atlem12  34898  lplncvrlvol2  34901  lvolcmp  34903  2lplnmj  34908  islinei  35026  linepmap  35061  lneq2at  35064  2llnma3r  35074  elpaddn0  35086  elpaddatriN  35089  elpaddat  35090  paddcom  35099  paddss1  35103  paddss2  35104  paddasslem6  35111  paddasslem7  35112  paddasslem10  35115  paddasslem15  35120  pmodlem2  35133  pmodl42N  35137  pmapjoin  35138  atmod1i1m  35144  llnmod1i2  35146  llnexchb2lem  35154  polcon2bN  35206  pclfinclN  35236  poml4N  35239  poml6N  35241  osumcllem11N  35252  osumclN  35253  pmapojoinN  35254  pexmidlem2N  35257  pexmidlem3N  35258  pexmidlem4N  35259  pexmidlem6N  35261  pexmidlem7N  35262  pl42lem2N  35266  pl42lem3N  35267  pl42lem4N  35268  pl42N  35269  lhpexle3lem  35297  lhpmcvr3  35311  lhp2at0nle  35321  lhprelat3N  35326  lauteq  35381  lautco  35383  ltrncoidN  35414  ltrneq2  35434  ltrnnidn  35461  ltrnideq  35462  trlnle  35473  cdlemc  35484  cdlemd4  35488  cdlemd5  35489  cdlemd9  35493  cdlemd  35494  ltrneq3  35495  cdlemefrs29pre00  35683  cdlemefrs29cpre1  35686  cdlemefrs29clN  35687  cdlemefrs32fva  35688  cdlemefr29exN  35690  cdlemefr27cl  35691  cdlemefs27cl  35701  cdlemefs32sn1aw  35702  cdleme32fva  35725  cdleme32d  35732  cdleme32f  35734  cdleme32le  35735  cdleme40n  35756  cdleme41snaw  35764  cdleme17d3  35784  cdleme48fvg  35788  cdlemeg46fvcl  35794  cdlemeg46fgN  35822  cdleme48fgv  35826  ltrniotavalbN  35872  cdlemb3  35894  cdlemg15  35944  cdlemg17dN  35951  trlco  36015  cdlemg44b  36020  ltrncom  36026  trljco  36028  tendococl  36060  tendoplcl  36069  tendoplcom  36070  tendotr  36118  cdlemk36  36201  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk19x  36231  cdlemk53b  36244  cdlemk55  36249  cdlemk35u  36252  cdlemk55u  36254  cdlemk39u  36256  cdlemk19u  36258  cdlemk56  36259  tendoex  36263  cdleml5N  36268  dihord2pre  36514  dihord6apre  36545  dihord5b  36548  dihord5apre  36551  dihord  36553  dihmeetlem1N  36579  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetbN  36592  dihmeetlem4preN  36595  dihmeetlem5  36597  dihmeetlem6  36598  dihmeetlem7N  36599  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem12N  36607  dihmeetlem13N  36608  dihmeetlem15N  36610  dihmeetlem17N  36612  dihmeetlem18N  36613  dihmeetlem19N  36614  dihmeetALTN  36616  dih1dimatlem0  36617  dihlspsnssN  36621  dvh3dim2  36737  mzpsubst  37311  diophrw  37322  eldioph2lem1  37323  rencldnfi  37385  pellexlem2  37394  pellqrexplicit  37441  infmrgelbi  37442  rmxycomplete  37482  congadd  37533  acongeq  37550  jm2.19  37560  jm2.22  37562  jm2.20nn  37564  jm2.25lem1  37565  jm2.27  37575  jm3.1  37587  lmhmlnmsplit  37657  pwssplit4  37659  hbtlem2  37694  dgraa0p  37719  idomrootle  37773  proot1hash  37778  iocunico  37796  relexpxpmin  38009  brtrclfv2  38019  ntrclsk3  38368  suprnmpt  39355  wessf1ornlem  39371  choicefi  39392  supxrgere  39549  supxrgelem  39553  supxrge  39554  infleinflem2  39587  snunioo1  39738  iccintsng  39749  fmul01  39812  lptre2pt  39872  0ellimcdiv  39881  fnlimfvre  39906  limsupmnfuzlem  39958  climisp  39978  limsupgtlem  40009  ibliccsinexp  40166  iblioosinexp  40168  volioc  40188  iblspltprt  40189  stoweidlem20  40237  stoweidlem22  40239  stoweidlem34  40251  stoweidlem44  40261  stoweidlem60  40277  wallispilem3  40284  fourierdlem42  40366  fourierdlem51  40374  fourierdlem54  40377  fourierdlem87  40410  fourierdlem97  40420  ioorrnopnlem  40524  sge0seq  40663  hoicvr  40762  ccatpfx  41409  pfxccat3  41426  lincresunit3lem3  42263  lindssnlvec  42275