Theorem simprr 537

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 495	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dfifp2dc  994  simp1rr  1094  simp2rr  1098  simp3rr  1102  elpr2elpr  3901  invdisjrab  4124  disjiun  4125  reg2exmidlema  4681  reg3exmidlemwe  4726  nnsucpred  4764  iotam  5369  fvmptt  5797  fcof1  5989  fliftfun  6002  isotr  6022  riotass2  6067  acexmidlemab  6079  ovmpodf  6220  fnmpoovd  6451  1stconst  6457  2ndconst  6458  cnvf1olem  6460  f1od2  6471  suppcofn  6506  smoiso  6573  tfrcldm  6634  tfrcl  6635  nntr2  6776  swoer  6835  erinxp  6883  ecopovsymg  6908  th3qlem1  6911  f1imaen2g  7080  pw2f1odclem  7134  mapdom1g  7147  fict  7170  fidifsnen  7172  dif1enen  7184  fiunsnnn  7185  fisbth  7187  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fimax2gtri  7206  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  ssfirab  7244  exmidssfi  7246  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlemi6  7279  sbthlemi8  7281  isbth  7284  fiuni  7312  supmaxti  7344  infminti  7367  ordiso2  7375  eldju2ndl  7412  eldju2ndr  7413  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctmlemr  7448  ctssdccl  7451  nninfninc  7463  fodjum  7486  fodju0  7487  omniwomnimkv  7507  exmidfodomrlemrALT  7555  acfun  7563  exmidaclem  7564  netap  7620  exmidmotap  7627  ccfunen  7630  cc1  7631  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  enq0sym  7799  enq0tr  7801  distrnq0  7826  prarloclem3  7864  genplt2i  7877  addlocpr  7903  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprg  7986  prplnqu  7987  addextpr  7988  recexprlemdisj  7997  recexprlemloc  7998  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  recexgt0sr  8140  mulgt0sr  8145  prsrriota  8155  suplocsrlem  8175  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axmulcom  8238  rereceu  8256  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  addcan  8507  addcan2  8508  addsub4  8570  ltadd2  8748  le2add  8773  lt2add  8774  lt2sub  8789  le2sub  8790  eqord1  8812  rereim  8916  apreap  8917  apreim  8933  mulreim  8934  apcotr  8937  apadd1  8938  addext  8940  apneg  8941  mulext1  8942  mulext  8944  ltleap  8962  aprcl  8976  mulap0  8984  mulcanapd  8991  recapb  9003  rec11ap  9042  rec11rap  9043  divdivdivap  9045  ddcanap  9058  divadddivap  9059  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  lemulge11  9198  lt2mul2div  9211  ltrec  9215  lerec  9216  lerec2  9221  ledivp1  9235  mulle0r  9276  nn0ge0div  9737  suprzclex  9748  qapne  10048  xrlelttr  10218  xrltletr  10219  xrre3  10234  xrrege0  10237  xaddge0  10290  xle2add  10291  xlt2add  10292  fzass4  10478  fzrev  10501  elfz1b  10507  eluzgtdifelfzo  10625  fzocatel  10627  zsupcllemstep  10672  zsupcllemex  10673  zssinfcl  10675  infssfzcldc  10679  infssfzledc  10680  suprzubdc  10681  exbtwnzlemex  10694  rebtwn2z  10699  modqid  10799  modqcyc  10809  modqaddabs  10812  modqaddmod  10813  mulqaddmodid  10814  modqadd2mod  10824  modqltm1p1mod  10826  modqsubmod  10832  modqsubmodmod  10833  modaddmodup  10837  modqmulmod  10839  modqmulmodr  10840  modqaddmulmod  10841  modqsubdir  10843  frec2uzisod  10857  uzennn  10886  iseqovex  10908  seqvalcd  10911  seq1g  10913  seqf  10914  seqovcd  10917  seqclg  10922  seqm1g  10924  seq3shft2  10931  seqshft2g  10932  monoord  10935  iseqf1olemnab  10951  seqf1oglem1  10969  seqf1og  10971  seqhomog  10980  seqfeq4g  10981  seq3distr  10982  expnegzap  11023  ltexp2a  11041  le2sq2  11065  bernneq  11111  expnlbnd2  11116  nn0ltexp2  11161  nn0opth2  11176  faclbnd  11193  bcval5  11215  hashcl  11234  hashen  11237  fihashdom  11257  hashunlem  11258  hashun  11259  hashxp  11281  hashmap  11282  fimaxq  11284  sseqn  11293  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  hashf1  11301  zfz1isolem1  11306  zfz1iso  11307  seq3coll  11308  sswrd  11327  ccatw2s1p1g  11427  ccatw2s1p2  11428  ccat2s1fstg  11430  wrdind  11508  pfxccatin12lem1  11514  pfxccatin12lem3  11518  reuccatpfxs1lem  11532  cvg1nlemres  11765  cvg1n  11766  resqrexlemp1rp  11786  resqrexlemoverl  11801  resqrexlemex  11805  sqrtsq  11824  abslt  11869  absle  11870  abs3lem  11892  maxleastlt  11996  maxltsup  11999  fimaxre2  12008  negfi  12009  xrmaxleastlt  12038  xrmaxltsup  12040  xrmaxaddlem  12042  2clim  12083  climcn2  12091  addcn2  12092  mulcn2  12094  reccn2ap  12095  climge0  12107  climcau  12129  fzf1o  12158  summodclem2  12165  summodc  12166  zsumdc  12167  fsumf1o  12173  fisumss  12175  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  mptfzshft  12225  fsumrev  12226  fsummulc2  12231  fsumconst  12237  modfsummod  12241  fsumrelem  12254  binom  12267  cvgratnn  12314  mertenslemub  12317  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodf1o  12371  fprodssdc  12373  fprodmul  12374  fprodcl2lem  12388  fprodrev  12402  fprodconst  12403  fprodap0  12404  fprodrec  12412  fprodap0f  12419  fprodle  12423  fprodmodd  12424  efcllem  12442  tanaddaplem  12521  moddvds  12582  dvdsflip  12634  oexpneg  12660  nn0o  12690  fldivndvdslt  12720  bitsfi  12740  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemeu  12800  dfgcd3  12803  dfgcd2  12807  dvdsmulgcd  12818  bezoutr  12825  nninfctlemfo  12833  lcmgcdlem  12871  coprmdvds2  12887  qredeu  12891  rpdvds  12893  cncongr1  12897  prmind2  12914  isprm5lem  12936  isprm6  12942  nnmaxpwlemparts  12968  nnmaxpw  12969  nonsq  13003  nn0sqdcq  13004  sqrtrirr  13005  hashdvds  13019  crth  13022  eulerthlemh  13029  prmdiveq  13034  hashgcdlem  13036  hashgcdeq  13038  nnnn0modprm0  13054  pclemub  13086  pceu  13094  pcmul  13100  pcqmul  13102  pcgcd1  13127  pc2dvds  13129  difsqpwdvds  13137  pcmpt  13142  prmpwdvds  13154  1arith  13166  mul4sq  13193  4sqlemafi  13194  4sqlemffi  13195  4sqexercise2  13198  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemg  13343  ennnfonelemex  13354  ennnfonelemrnh  13356  ennnfonelemf1  13358  ennnfonelemrn  13359  ennnfonelemdm  13360  ennnfonelemim  13364  ennnfone  13365  ctinf  13370  ctiunctlemfo  13379  nninfdclemcl  13388  nninfdclemf  13389  nninfdclemp1  13390  unbendc  13394  isstruct2r  13412  setscom  13441  ercpbl  13701  opifismgmdc  13740  grpinvalem  13754  gzsumvalx  13758  gzsumfzval  13760  gzsumval2  13763  sgrppropd  13777  mndpropd  13802  issubmnd  13804  submnd0  13806  mhmf1o  13826  subsubm  13839  0mhm  13842  resmhm  13843  mhmco  13846  mhmima  13847  mhmeql  13848  gzsumwsubmcl  13850  gzsumcl  13853  grprcan  13891  grpinvid1  13906  grpinvid2  13907  grplcan  13916  grplmulf1o  13928  grpnpncan0  13950  dfgrp3mlem  13952  grplactcnv  13956  mulgval  13974  mulgfng  13976  mulgnngzsum  13979  mulg1  13981  mulgnnp1  13982  mulgneg  13992  mulgnndir  14003  mulgdirlem  14005  mulgnn0ass  14010  mulgass  14011  subgmulg  14040  issubg4m  14045  subsubg  14049  subgintm  14050  isnsg3  14059  eqgcpbl  14080  ghmeql  14119  ghmnsgima  14120  ghmnsgpreima  14121  ghmf1  14125  ghmf1o  14127  conjghm  14128  qusghm  14134  cmnsubm  14161  ablpncan3  14170  invghm  14182  eqgabl  14183  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gsumvalfi  14201  gsumzfi  14207  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  gsumconstcmn  14215  prdssgrpd  14240  prdsmndd  14243  pwssub  14265  rngpropd  14303  imasrng  14304  qusrng  14306  srglmhm  14346  srgrmhm  14347  ringpropd  14392  ringlghm  14415  ringrghm  14416  imasring  14418  qusring2  14420  opprrngbg  14432  dvdsrvald  14449  dvdsrd  14450  dvdsrex  14454  dvdsrtr  14457  unitpropdg  14504  rhmopp  14532  isnzr2  14540  issubrng2  14567  subrngintm  14569  subsubrng  14571  subrgintm  14600  subsubrg  14602  rhmpropd  14611  ringunitap  14642  aprap  14647  drngunitap  14657  lmodprop2d  14734  rmodislmod  14737  lssvacl  14751  lssvsubcl  14752  lssvscl  14761  islss3  14765  lss1d  14769  rnglidlmcl  14866  2idlcpblrng  14909  crngridl  14916  gsumfsum  14972  expghmap  14991  mulgghm2  14992  mulgrhm  14993  znf1o  15035  znleval  15037  znidom  15041  znidomb  15042  znunit  15043  asclghm  15074  issubassa2  15084  assamulgscmlem2  15091  psrbagcon  15111  mplsubgfilemcl  15139  iuncld  15265  ssnei2  15307  topssnei  15312  restopnb  15331  cnfval  15344  cnpfval  15345  iscnp4  15368  cnptopco  15372  cncnpi  15378  cncnp  15380  cnconst2  15383  cnrest2  15386  cnptoprest  15389  cnptoprest2  15390  cnpdis  15392  lmss  15396  lmtopcnp  15400  neitx  15418  txcnp  15421  txrest  15426  txdis1cn  15428  txlm  15429  cnmpt21  15441  imasnopn  15449  xmetres2  15529  blvalps  15538  blval  15539  elbl2ps  15542  elbl2  15543  blhalf  15558  blssexps  15579  blssex  15580  ssblex  15581  blin2  15582  bdmetval  15650  xmetxp  15657  xmettx  15660  metcnpi3  15667  txmetcnp  15668  addcncntoplem  15711  fsumcncntop  15717  elcncf2  15724  mulc1cncf  15739  cncfco  15741  cncfmet  15742  cncfmptc  15746  mulcncf  15758  dedekindeulemub  15768  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeu  15773  dedekindicclemub  15777  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicclemicc  15782  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemuopn  15788  dich0  15802  limcimo  15815  cnplimccntop  15820  limccnp2lem  15826  limccnp2cntop  15827  dvfvalap  15831  dveflem  15876  plycolemc  15908  plyco  15909  plyrecj  15913  reeff1olem  15921  reeff1oleme  15922  eflt  15925  sin0pilem2  15933  pilem3  15934  ioocosf1o  16005  logdivlt  16046  logdivle  16047  cxplt  16071  cxple  16072  cxplt3  16075  apcxp2  16094  rprelogbmul  16110  rprelogbdiv  16112  logbgt0b  16121  logbgcd1irrap  16125  zprmlogbap  16137  pellexlem3  16150  ppinprm  16171  mpodvdsmulf1o  16185  fsumdvdsmul  16186  bposlem3  16211  lgsdir2lem5  16249  lgsdi  16254  lgsne0  16255  gausslemma2dlem1f1o  16277  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem2  16299  lgsquad2  16300  2sqlem6  16337  2sqlem8  16340  2sqlem9  16341  2sqlem10  16342  upgredg  16483  usgredg4  16554  uspgredg2vlem  16559  usgr1eop  16584  upgrspanop  16622  umgrspanop  16623  usgrspanop  16624  vtxedgfi  16628  vtxlpfi  16629  iswlkg  16668  upgriswlkdc  16699  upgr2wlkdc  16716  clwwlkccatlem  16739  clwwlknonex2e  16779  nnti  17120  pwtrufal  17125  pwf1oexmid  17127  sssneq  17130  qdencn  17170  cvgcmp2n  17180  trilpolemlt1  17188  trirec0  17191  qdiff  17196  redc0  17205  reap0  17206  cndcap  17207  nconstwlpolemgt0  17212  neap0mkv  17217  supfz  17219  inffz  17220