Theorem simprr 533

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

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

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2	1	ad2antll 491	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  dfifp2dc  990  simp1rr  1090  simp2rr  1094  simp3rr  1098  elpr2elpr  3864  invdisjrab  4087  disjiun  4088  reg2exmidlema  4638  reg3exmidlemwe  4683  nnsucpred  4721  iotam  5325  fvmptt  5747  fcof1  5934  fliftfun  5947  isotr  5967  riotass2  6010  acexmidlemab  6022  ovmpodf  6163  fnmpoovd  6389  1stconst  6395  2ndconst  6396  cnvf1olem  6398  f1od2  6409  suppcofn  6444  smoiso  6511  tfrcldm  6572  tfrcl  6573  nntr2  6714  swoer  6773  erinxp  6821  ecopovsymg  6846  th3qlem1  6849  f1imaen2g  7010  pw2f1odclem  7063  mapdom1g  7076  fict  7098  fidifsnen  7100  dif1enen  7112  fiunsnnn  7113  fisbth  7115  findcard2d  7123  findcard2sd  7124  diffifi  7126  ac6sfi  7130  fimax2gtri  7134  nnwetri  7151  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  fisseneq  7170  ssfirab  7172  exmidssfi  7174  fidcenumlemrk  7196  fidcenumlemr  7197  sbthlemi6  7204  sbthlemi8  7206  isbth  7209  fiuni  7220  supmaxti  7246  infminti  7269  ordiso2  7277  eldju2ndl  7314  eldju2ndr  7315  omp1eomlem  7336  difinfsnlem  7341  difinfinf  7343  ctmlemr  7350  ctssdccl  7353  nninfninc  7365  fodjum  7388  fodju0  7389  omniwomnimkv  7409  exmidfodomrlemrALT  7457  acfun  7465  exmidaclem  7466  netap  7516  exmidmotap  7523  ccfunen  7526  cc1  7527  cc2lem  7528  dfplpq2  7617  dfmpq2  7618  mulpipqqs  7636  distrnqg  7650  enq0sym  7695  enq0tr  7697  distrnq0  7722  prarloclem3  7760  genplt2i  7773  addlocpr  7799  prmuloc  7829  distrlem1prl  7845  distrlem1pru  7846  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemfl  7872  ltexprlemrl  7873  ltexprlemfu  7874  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltaprg  7882  prplnqu  7883  addextpr  7884  recexprlemdisj  7893  recexprlemloc  7894  aptiprleml  7902  aptiprlemu  7903  ltmprr  7905  archpr  7906  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlem1  7922  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnjltk  7954  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemdisj  7965  caucvgprprlemloc  7966  caucvgprprlemaddq  7971  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  recexgt0sr  8036  mulgt0sr  8041  prsrriota  8051  suplocsrlem  8071  addcnsr  8097  mulcnsr  8098  mulcnsrec  8106  axmulcom  8134  rereceu  8152  axarch  8154  axcaucvglemres  8162  axpre-suploclemres  8164  lelttr  8310  ltletr  8311  addcan  8401  addcan2  8402  addsub4  8464  ltadd2  8641  le2add  8666  lt2add  8667  lt2sub  8682  le2sub  8683  eqord1  8705  rereim  8808  apreap  8809  apreim  8825  mulreim  8826  apcotr  8829  apadd1  8830  addext  8832  apneg  8833  mulext1  8834  mulext  8836  ltleap  8854  aprcl  8868  mulap0  8876  mulcanapd  8883  recapb  8893  rec11ap  8932  rec11rap  8933  divdivdivap  8935  ddcanap  8948  divadddivap  8949  prodgt0gt0  9073  prodgt0  9074  prodge0  9076  lemulge11  9088  lt2mul2div  9101  ltrec  9105  lerec  9106  lerec2  9111  ledivp1  9125  mulle0r  9166  nn0ge0div  9611  suprzclex  9622  qapne  9917  xrlelttr  10085  xrltletr  10086  xrre3  10101  xrrege0  10104  xaddge0  10157  xle2add  10158  xlt2add  10159  fzass4  10342  fzrev  10364  elfz1b  10370  eluzgtdifelfzo  10488  fzocatel  10490  zsupcllemstep  10535  zsupcllemex  10536  zssinfcl  10538  suprzubdc  10542  exbtwnzlemex  10555  rebtwn2z  10560  modqid  10657  modqcyc  10667  modqaddabs  10670  modqaddmod  10671  mulqaddmodid  10672  modqadd2mod  10682  modqltm1p1mod  10684  modqsubmod  10690  modqsubmodmod  10691  modaddmodup  10695  modqmulmod  10697  modqmulmodr  10698  modqaddmulmod  10699  modqsubdir  10701  frec2uzisod  10715  uzennn  10744  iseqovex  10766  seqvalcd  10769  seq1g  10771  seqf  10772  seqovcd  10775  seqclg  10780  seqm1g  10782  seq3shft2  10789  seqshft2g  10790  monoord  10793  iseqf1olemnab  10809  seqf1oglem1  10827  seqf1og  10829  seqhomog  10838  seqfeq4g  10839  seq3distr  10840  expnegzap  10881  ltexp2a  10899  le2sq2  10923  bernneq  10968  expnlbnd2  10973  nn0ltexp2  11017  nn0opth2  11032  faclbnd  11049  bcval5  11071  hashcl  11089  hashen  11092  fihashdom  11112  hashunlem  11113  hashun  11114  hashxp  11136  fimaxq  11137  zfz1isolem1  11150  zfz1iso  11151  seq3coll  11152  sswrd  11171  ccatw2s1p1g  11271  ccatw2s1p2  11272  ccat2s1fstg  11274  wrdind  11352  pfxccatin12lem1  11358  pfxccatin12lem3  11362  reuccatpfxs1lem  11376  cvg1nlemres  11608  cvg1n  11609  resqrexlemp1rp  11629  resqrexlemoverl  11644  resqrexlemex  11648  sqrtsq  11667  abslt  11711  absle  11712  abs3lem  11734  maxleastlt  11838  maxltsup  11841  fimaxre2  11850  negfi  11851  xrmaxleastlt  11879  xrmaxltsup  11881  xrmaxaddlem  11883  2clim  11924  climcn2  11932  addcn2  11933  mulcn2  11935  reccn2ap  11936  climge0  11948  climcau  11970  fzf1o  11999  summodclem2  12006  summodc  12007  zsumdc  12008  fsumf1o  12014  fisumss  12016  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  mptfzshft  12066  fsumrev  12067  fsummulc2  12072  fsumconst  12078  modfsummod  12082  fsumrelem  12095  binom  12108  cvgratnn  12155  mertenslemub  12158  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  fprodcl2lem  12229  fprodrev  12243  fprodconst  12244  fprodap0  12245  fprodrec  12253  fprodap0f  12260  fprodle  12264  fprodmodd  12265  efcllem  12283  tanaddaplem  12362  moddvds  12423  dvdsflip  12475  oexpneg  12501  nn0o  12531  fldivndvdslt  12561  bitsfi  12581  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemeu  12641  dfgcd3  12644  dfgcd2  12648  dvdsmulgcd  12659  bezoutr  12666  nninfctlemfo  12674  lcmgcdlem  12712  coprmdvds2  12728  qredeu  12732  rpdvds  12734  cncongr1  12738  prmind2  12755  isprm5lem  12776  isprm6  12782  oddpwdclemdc  12808  nonsq  12842  hashdvds  12856  crth  12859  eulerthlemh  12866  prmdiveq  12871  hashgcdlem  12873  hashgcdeq  12875  nnnn0modprm0  12891  pclemub  12923  pceu  12931  pcmul  12937  pcqmul  12939  pcgcd1  12964  pc2dvds  12966  difsqpwdvds  12974  pcmpt  12979  prmpwdvds  12991  1arith  13003  mul4sq  13030  4sqlemafi  13031  4sqlemffi  13032  4sqexercise2  13035  ennnfonelemg  13087  ennnfonelemex  13098  ennnfonelemrnh  13100  ennnfonelemf1  13102  ennnfonelemrn  13103  ennnfonelemdm  13104  ennnfonelemim  13108  ennnfone  13109  ctinf  13114  ctiunctlemfo  13123  nninfdclemcl  13132  nninfdclemf  13133  nninfdclemp1  13134  unbendc  13138  isstruct2r  13156  setscom  13185  ercpbl  13477  opifismgmdc  13517  grpinvalem  13531  igsumvalx  13535  gsumfzval  13537  gsumval2  13543  sgrppropd  13559  prdssgrpd  13561  mndpropd  13586  issubmnd  13588  submnd0  13590  prdsmndd  13594  mhmf1o  13616  subsubm  13629  0mhm  13632  resmhm  13633  mhmco  13636  mhmima  13637  mhmeql  13638  gsumfzz  13641  gsumwsubmcl  13642  gsumfzcl  13645  grprcan  13683  grpinvid1  13698  grpinvid2  13699  grplcan  13708  grplmulf1o  13720  grpnpncan0  13742  dfgrp3mlem  13744  grplactcnv  13748  pwssub  13759  mulgval  13772  mulgfng  13774  mulgnngsum  13777  mulg1  13779  mulgnnp1  13780  mulgneg  13790  mulgnndir  13801  mulgdirlem  13803  mulgnn0ass  13808  mulgass  13809  subgmulg  13838  issubg4m  13843  subsubg  13847  subgintm  13848  isnsg3  13857  eqgcpbl  13878  ghmeql  13917  ghmnsgima  13918  ghmnsgpreima  13919  ghmf1  13923  ghmf1o  13925  conjghm  13926  qusghm  13932  ablpncan3  13967  invghm  13979  eqgabl  13980  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  rngpropd  14032  imasrng  14033  qusrng  14035  srglmhm  14070  srgrmhm  14071  ringpropd  14115  ringlghm  14138  ringrghm  14139  imasring  14141  qusring2  14143  opprrngbg  14155  dvdsrvald  14171  dvdsrd  14172  dvdsrex  14176  dvdsrtr  14179  unitpropdg  14226  rhmopp  14254  isnzr2  14262  issubrng2  14288  subrngintm  14290  subsubrng  14292  subrgintm  14321  subsubrg  14323  rhmpropd  14332  aprap  14365  lmodprop2d  14427  rmodislmod  14430  lssvacl  14444  lssvsubcl  14445  lssvscl  14454  islss3  14458  lss1d  14462  rnglidlmcl  14559  2idlcpblrng  14602  crngridl  14609  expghmap  14686  mulgghm2  14687  mulgrhm  14688  znf1o  14730  znleval  14732  znidom  14736  znidomb  14737  znunit  14738  psrbagcon  14755  mplsubgfilemcl  14783  iuncld  14909  ssnei2  14951  topssnei  14956  restopnb  14975  cnfval  14988  cnpfval  14989  iscnp4  15012  cnptopco  15016  cncnpi  15022  cncnp  15024  cnconst2  15027  cnrest2  15030  cnptoprest  15033  cnptoprest2  15034  cnpdis  15036  lmss  15040  lmtopcnp  15044  neitx  15062  txcnp  15065  txrest  15070  txdis1cn  15072  txlm  15073  cnmpt21  15085  imasnopn  15093  xmetres2  15173  blvalps  15182  blval  15183  elbl2ps  15186  elbl2  15187  blhalf  15202  blssexps  15223  blssex  15224  ssblex  15225  blin2  15226  bdmetval  15294  xmetxp  15301  xmettx  15304  metcnpi3  15311  txmetcnp  15312  addcncntoplem  15355  fsumcncntop  15361  elcncf2  15368  mulc1cncf  15383  cncfco  15385  cncfmet  15386  cncfmptc  15390  mulcncf  15402  dedekindeulemub  15412  dedekindeulemloc  15413  dedekindeulemlu  15415  dedekindeu  15417  dedekindicclemub  15421  dedekindicclemloc  15422  dedekindicclemlu  15424  dedekindicclemicc  15426  dedekindicc  15427  ivthinclemlopn  15430  ivthinclemuopn  15432  dich0  15446  limcimo  15459  cnplimccntop  15464  limccnp2lem  15470  limccnp2cntop  15471  dvfvalap  15475  dveflem  15520  plycolemc  15552  plyco  15553  plyrecj  15557  reeff1olem  15565  reeff1oleme  15566  eflt  15569  sin0pilem2  15576  pilem3  15577  ioocosf1o  15648  cxplt  15710  cxple  15711  cxplt3  15714  apcxp2  15733  rprelogbmul  15749  rprelogbdiv  15751  logbgt0b  15760  logbgcd1irrap  15764  pellexlem3  15776  mpodvdsmulf1o  15787  fsumdvdsmul  15788  lgsdir2lem5  15834  lgsdi  15839  lgsne0  15840  gausslemma2dlem1f1o  15862  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem2  15884  lgsquad2  15885  2sqlem6  15922  2sqlem8  15925  2sqlem9  15926  2sqlem10  15927  upgredg  16068  usgredg4  16139  uspgredg2vlem  16144  usgr1eop  16169  upgrspanop  16207  umgrspanop  16208  usgrspanop  16209  vtxedgfi  16213  vtxlpfi  16214  iswlkg  16253  upgriswlkdc  16284  upgr2wlkdc  16301  clwwlkccatlem  16324  clwwlknonex2e  16364  nnti  16695  pwtrufal  16702  pwf1oexmid  16704  sssneq  16707  qdencn  16738  cvgcmp2n  16748  trilpolemlt1  16756  trirec0  16759  qdiff  16764  redc0  16773  reap0  16774  cndcap  16775  nconstwlpolemgt0  16780  neap0mkv  16785  supfz  16787  inffz  16788  gfsumval  16792  gfsumcl  16799