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  3885  invdisjrab  4108  disjiun  4109  reg2exmidlema  4661  reg3exmidlemwe  4706  nnsucpred  4744  iotam  5349  fvmptt  5774  fcof1  5962  fliftfun  5975  isotr  5995  riotass2  6040  acexmidlemab  6052  ovmpodf  6193  fnmpoovd  6424  1stconst  6430  2ndconst  6431  cnvf1olem  6433  f1od2  6444  suppcofn  6479  smoiso  6546  tfrcldm  6607  tfrcl  6608  nntr2  6749  swoer  6808  erinxp  6856  ecopovsymg  6881  th3qlem1  6884  f1imaen2g  7046  pw2f1odclem  7100  mapdom1g  7113  fict  7136  fidifsnen  7138  dif1enen  7150  fiunsnnn  7151  fisbth  7153  findcard2d  7161  findcard2sd  7162  diffifi  7164  ac6sfi  7168  fimax2gtri  7172  nnwetri  7189  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fisseneq  7208  ssfirab  7210  exmidssfi  7212  fidcenumlemrk  7237  fidcenumlemr  7238  sbthlemi6  7245  sbthlemi8  7247  isbth  7250  fiuni  7278  supmaxti  7308  infminti  7331  ordiso2  7339  eldju2ndl  7376  eldju2ndr  7377  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctmlemr  7412  ctssdccl  7415  nninfninc  7427  fodjum  7450  fodju0  7451  omniwomnimkv  7471  exmidfodomrlemrALT  7519  acfun  7527  exmidaclem  7528  netap  7584  exmidmotap  7591  ccfunen  7594  cc1  7595  cc2lem  7596  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  distrnqg  7718  enq0sym  7763  enq0tr  7765  distrnq0  7790  prarloclem3  7828  genplt2i  7841  addlocpr  7867  prmuloc  7897  distrlem1prl  7913  distrlem1pru  7914  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltaprg  7950  prplnqu  7951  addextpr  7952  recexprlemdisj  7961  recexprlemloc  7962  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  archpr  7974  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprprlemnkltj  8020  caucvgprprlemnkeqj  8021  caucvgprprlemnjltk  8022  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  caucvgprprlemaddq  8039  suplocexprlemrl  8048  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemex  8053  suplocexprlemub  8054  recexgt0sr  8104  mulgt0sr  8109  prsrriota  8119  suplocsrlem  8139  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axmulcom  8202  rereceu  8220  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  lelttr  8378  ltletr  8379  addcan  8469  addcan2  8470  addsub4  8532  ltadd2  8710  le2add  8735  lt2add  8736  lt2sub  8751  le2sub  8752  eqord1  8774  rereim  8877  apreap  8878  apreim  8894  mulreim  8895  apcotr  8898  apadd1  8899  addext  8901  apneg  8902  mulext1  8903  mulext  8905  ltleap  8923  aprcl  8937  mulap0  8945  mulcanapd  8952  recapb  8962  rec11ap  9001  rec11rap  9002  divdivdivap  9004  ddcanap  9017  divadddivap  9018  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  lemulge11  9157  lt2mul2div  9170  ltrec  9174  lerec  9175  lerec2  9180  ledivp1  9194  mulle0r  9235  nn0ge0div  9683  suprzclex  9694  qapne  9989  xrlelttr  10158  xrltletr  10159  xrre3  10174  xrrege0  10177  xaddge0  10230  xle2add  10231  xlt2add  10232  fzass4  10417  fzrev  10440  elfz1b  10446  eluzgtdifelfzo  10564  fzocatel  10566  zsupcllemstep  10611  zsupcllemex  10612  zssinfcl  10614  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  exbtwnzlemex  10633  rebtwn2z  10638  modqid  10735  modqcyc  10745  modqaddabs  10748  modqaddmod  10749  mulqaddmodid  10750  modqadd2mod  10760  modqltm1p1mod  10762  modqsubmod  10768  modqsubmodmod  10769  modaddmodup  10773  modqmulmod  10775  modqmulmodr  10776  modqaddmulmod  10777  modqsubdir  10779  frec2uzisod  10793  uzennn  10822  iseqovex  10844  seqvalcd  10847  seq1g  10849  seqf  10850  seqovcd  10853  seqclg  10858  seqm1g  10860  seq3shft2  10867  seqshft2g  10868  monoord  10871  iseqf1olemnab  10887  seqf1oglem1  10905  seqf1og  10907  seqhomog  10916  seqfeq4g  10917  seq3distr  10918  expnegzap  10959  ltexp2a  10977  le2sq2  11001  bernneq  11047  expnlbnd2  11052  nn0ltexp2  11096  nn0opth2  11111  faclbnd  11128  bcval5  11150  hashcl  11169  hashen  11172  fihashdom  11192  hashunlem  11193  hashun  11194  hashxp  11216  hashmap  11217  fimaxq  11219  sseqn  11228  hashfibclem  11231  hashfibc  11232  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  sswrd  11258  ccatw2s1p1g  11358  ccatw2s1p2  11359  ccat2s1fstg  11361  wrdind  11439  pfxccatin12lem1  11445  pfxccatin12lem3  11449  reuccatpfxs1lem  11463  cvg1nlemres  11695  cvg1n  11696  resqrexlemp1rp  11716  resqrexlemoverl  11731  resqrexlemex  11735  sqrtsq  11754  abslt  11798  absle  11799  abs3lem  11821  maxleastlt  11925  maxltsup  11928  fimaxre2  11937  negfi  11938  xrmaxleastlt  11966  xrmaxltsup  11968  xrmaxaddlem  11970  2clim  12011  climcn2  12019  addcn2  12020  mulcn2  12022  reccn2ap  12023  climge0  12035  climcau  12057  fzf1o  12086  summodclem2  12093  summodc  12094  zsumdc  12095  fsumf1o  12101  fisumss  12103  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  mptfzshft  12153  fsumrev  12154  fsummulc2  12159  fsumconst  12165  modfsummod  12169  fsumrelem  12182  binom  12195  cvgratnn  12242  mertenslemub  12245  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodf1o  12299  fprodssdc  12301  fprodmul  12302  fprodcl2lem  12316  fprodrev  12330  fprodconst  12331  fprodap0  12332  fprodrec  12340  fprodap0f  12347  fprodle  12351  fprodmodd  12352  efcllem  12370  tanaddaplem  12449  moddvds  12510  dvdsflip  12562  oexpneg  12588  nn0o  12618  fldivndvdslt  12648  bitsfi  12668  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlemeu  12728  dfgcd3  12731  dfgcd2  12735  dvdsmulgcd  12746  bezoutr  12753  nninfctlemfo  12761  lcmgcdlem  12799  coprmdvds2  12815  qredeu  12819  rpdvds  12821  cncongr1  12825  prmind2  12842  isprm5lem  12863  isprm6  12869  oddpwdclemdc  12895  nonsq  12929  hashdvds  12943  crth  12946  eulerthlemh  12953  prmdiveq  12958  hashgcdlem  12960  hashgcdeq  12962  nnnn0modprm0  12978  pclemub  13010  pceu  13018  pcmul  13024  pcqmul  13026  pcgcd1  13051  pc2dvds  13053  difsqpwdvds  13061  pcmpt  13066  prmpwdvds  13078  1arith  13090  mul4sq  13117  4sqlemafi  13118  4sqlemffi  13119  4sqexercise2  13122  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemg  13238  ennnfonelemex  13249  ennnfonelemrnh  13251  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemdm  13255  ennnfonelemim  13259  ennnfone  13260  ctinf  13265  ctiunctlemfo  13274  nninfdclemcl  13283  nninfdclemf  13284  nninfdclemp1  13285  unbendc  13289  isstruct2r  13307  setscom  13336  ercpbl  13595  opifismgmdc  13634  grpinvalem  13648  igsumvalx  13652  gsumfzval  13654  gsumval2  13660  sgrppropd  13676  mndpropd  13701  issubmnd  13703  submnd0  13705  mhmf1o  13725  subsubm  13738  0mhm  13741  resmhm  13742  mhmco  13745  mhmima  13746  mhmeql  13747  gsumfzz  13750  gsumwsubmcl  13751  gsumfzcl  13754  grprcan  13792  grpinvid1  13807  grpinvid2  13808  grplcan  13817  grplmulf1o  13829  grpnpncan0  13851  dfgrp3mlem  13853  grplactcnv  13857  mulgval  13875  mulgfng  13877  mulgnngsum  13880  mulg1  13882  mulgnnp1  13883  mulgneg  13893  mulgnndir  13904  mulgdirlem  13906  mulgnn0ass  13911  mulgass  13912  subgmulg  13941  issubg4m  13946  subsubg  13950  subgintm  13951  isnsg3  13960  eqgcpbl  13981  ghmeql  14020  ghmnsgima  14021  ghmnsgpreima  14022  ghmf1  14026  ghmf1o  14028  conjghm  14029  qusghm  14035  ablpncan3  14070  invghm  14082  eqgabl  14083  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gfsumval  14102  gfsumz  14109  gfsumcl  14110  prdssgrpd  14133  prdsmndd  14136  pwssub  14158  rngpropd  14194  imasrng  14195  qusrng  14197  srglmhm  14236  srgrmhm  14237  ringpropd  14281  ringlghm  14304  ringrghm  14305  imasring  14307  qusring2  14309  opprrngbg  14321  dvdsrvald  14338  dvdsrd  14339  dvdsrex  14343  dvdsrtr  14346  unitpropdg  14393  rhmopp  14421  isnzr2  14429  issubrng2  14456  subrngintm  14458  subsubrng  14460  subrgintm  14489  subsubrg  14491  rhmpropd  14500  ringunitap  14531  aprap  14536  drngunitap  14546  lmodprop2d  14622  rmodislmod  14625  lssvacl  14639  lssvsubcl  14640  lssvscl  14649  islss3  14653  lss1d  14657  rnglidlmcl  14754  2idlcpblrng  14797  crngridl  14804  expghmap  14881  mulgghm2  14882  mulgrhm  14883  znf1o  14925  znleval  14927  znidom  14931  znidomb  14932  znunit  14933  psrbagcon  14952  mplsubgfilemcl  14980  iuncld  15106  ssnei2  15148  topssnei  15153  restopnb  15172  cnfval  15185  cnpfval  15186  iscnp4  15209  cnptopco  15213  cncnpi  15219  cncnp  15221  cnconst2  15224  cnrest2  15227  cnptoprest  15230  cnptoprest2  15231  cnpdis  15233  lmss  15237  lmtopcnp  15241  neitx  15259  txcnp  15262  txrest  15267  txdis1cn  15269  txlm  15270  cnmpt21  15282  imasnopn  15290  xmetres2  15370  blvalps  15379  blval  15380  elbl2ps  15383  elbl2  15384  blhalf  15399  blssexps  15420  blssex  15421  ssblex  15422  blin2  15423  bdmetval  15491  xmetxp  15498  xmettx  15501  metcnpi3  15508  txmetcnp  15509  addcncntoplem  15552  fsumcncntop  15558  elcncf2  15565  mulc1cncf  15580  cncfco  15582  cncfmet  15583  cncfmptc  15587  mulcncf  15599  dedekindeulemub  15609  dedekindeulemloc  15610  dedekindeulemlu  15612  dedekindeu  15614  dedekindicclemub  15618  dedekindicclemloc  15619  dedekindicclemlu  15621  dedekindicclemicc  15623  dedekindicc  15624  ivthinclemlopn  15627  ivthinclemuopn  15629  dich0  15643  limcimo  15656  cnplimccntop  15661  limccnp2lem  15667  limccnp2cntop  15668  dvfvalap  15672  dveflem  15717  plycolemc  15749  plyco  15750  plyrecj  15754  reeff1olem  15762  reeff1oleme  15763  eflt  15766  sin0pilem2  15773  pilem3  15774  ioocosf1o  15845  cxplt  15907  cxple  15908  cxplt3  15911  apcxp2  15930  rprelogbmul  15946  rprelogbdiv  15948  logbgt0b  15957  logbgcd1irrap  15961  pellexlem3  15973  mpodvdsmulf1o  15984  fsumdvdsmul  15985  lgsdir2lem5  16031  lgsdi  16036  lgsne0  16037  gausslemma2dlem1f1o  16059  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem2  16081  lgsquad2  16082  2sqlem6  16119  2sqlem8  16122  2sqlem9  16123  2sqlem10  16124  upgredg  16265  usgredg4  16336  uspgredg2vlem  16341  usgr1eop  16366  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  vtxedgfi  16410  vtxlpfi  16411  iswlkg  16450  upgriswlkdc  16481  upgr2wlkdc  16498  clwwlkccatlem  16521  clwwlknonex2e  16561  nnti  16892  pwtrufal  16897  pwf1oexmid  16899  sssneq  16902  qdencn  16933  cvgcmp2n  16943  trilpolemlt1  16951  trirec0  16954  qdiff  16959  redc0  16968  reap0  16969  cndcap  16970  nconstwlpolemgt0  16976  neap0mkv  16981  supfz  16983  inffz  16984