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  3880  invdisjrab  4103  disjiun  4104  reg2exmidlema  4656  reg3exmidlemwe  4701  nnsucpred  4739  iotam  5344  fvmptt  5769  fcof1  5956  fliftfun  5969  isotr  5989  riotass2  6032  acexmidlemab  6044  ovmpodf  6185  fnmpoovd  6411  1stconst  6417  2ndconst  6418  cnvf1olem  6420  f1od2  6431  suppcofn  6466  smoiso  6533  tfrcldm  6594  tfrcl  6595  nntr2  6736  swoer  6795  erinxp  6843  ecopovsymg  6868  th3qlem1  6871  f1imaen2g  7033  pw2f1odclem  7087  mapdom1g  7100  fict  7123  fidifsnen  7125  dif1enen  7137  fiunsnnn  7138  fisbth  7140  findcard2d  7148  findcard2sd  7149  diffifi  7151  ac6sfi  7155  fimax2gtri  7159  nnwetri  7176  unsnfi  7179  unsnfidcex  7180  unsnfidcel  7181  fisseneq  7195  ssfirab  7197  exmidssfi  7199  fidcenumlemrk  7224  fidcenumlemr  7225  sbthlemi6  7232  sbthlemi8  7234  isbth  7237  fiuni  7265  supmaxti  7295  infminti  7318  ordiso2  7326  eldju2ndl  7363  eldju2ndr  7364  omp1eomlem  7385  difinfsnlem  7390  difinfinf  7392  ctmlemr  7399  ctssdccl  7402  nninfninc  7414  fodjum  7437  fodju0  7438  omniwomnimkv  7458  exmidfodomrlemrALT  7506  acfun  7514  exmidaclem  7515  netap  7568  exmidmotap  7575  ccfunen  7578  cc1  7579  cc2lem  7580  dfplpq2  7669  dfmpq2  7670  mulpipqqs  7688  distrnqg  7702  enq0sym  7747  enq0tr  7749  distrnq0  7774  prarloclem3  7812  genplt2i  7825  addlocpr  7851  prmuloc  7881  distrlem1prl  7897  distrlem1pru  7898  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  ltaprg  7934  prplnqu  7935  addextpr  7936  recexprlemdisj  7945  recexprlemloc  7946  aptiprleml  7954  aptiprlemu  7955  ltmprr  7957  archpr  7958  cauappcvgprlemopl  7961  cauappcvgprlemopu  7963  cauappcvgprlemdisj  7966  cauappcvgprlemloc  7967  cauappcvgprlem1  7974  cauappcvgprlemlim  7976  caucvgprlemnkj  7981  caucvgprlemopl  7984  caucvgprlemopu  7986  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemnjltk  8006  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemdisj  8017  caucvgprprlemloc  8018  caucvgprprlemaddq  8023  suplocexprlemrl  8032  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemloc  8036  suplocexprlemex  8037  suplocexprlemub  8038  recexgt0sr  8088  mulgt0sr  8093  prsrriota  8103  suplocsrlem  8123  addcnsr  8149  mulcnsr  8150  mulcnsrec  8158  axmulcom  8186  rereceu  8204  axarch  8206  axcaucvglemres  8214  axpre-suploclemres  8216  lelttr  8362  ltletr  8363  addcan  8453  addcan2  8454  addsub4  8516  ltadd2  8693  le2add  8718  lt2add  8719  lt2sub  8734  le2sub  8735  eqord1  8757  rereim  8860  apreap  8861  apreim  8877  mulreim  8878  apcotr  8881  apadd1  8882  addext  8884  apneg  8885  mulext1  8886  mulext  8888  ltleap  8906  aprcl  8920  mulap0  8928  mulcanapd  8935  recapb  8945  rec11ap  8984  rec11rap  8985  divdivdivap  8987  ddcanap  9000  divadddivap  9001  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  lemulge11  9140  lt2mul2div  9153  ltrec  9157  lerec  9158  lerec2  9163  ledivp1  9177  mulle0r  9218  nn0ge0div  9665  suprzclex  9676  qapne  9971  xrlelttr  10139  xrltletr  10140  xrre3  10155  xrrege0  10158  xaddge0  10211  xle2add  10212  xlt2add  10213  fzass4  10396  fzrev  10418  elfz1b  10424  eluzgtdifelfzo  10542  fzocatel  10544  zsupcllemstep  10589  zsupcllemex  10590  zssinfcl  10592  suprzubdc  10596  exbtwnzlemex  10609  rebtwn2z  10614  modqid  10711  modqcyc  10721  modqaddabs  10724  modqaddmod  10725  mulqaddmodid  10726  modqadd2mod  10736  modqltm1p1mod  10738  modqsubmod  10744  modqsubmodmod  10745  modaddmodup  10749  modqmulmod  10751  modqmulmodr  10752  modqaddmulmod  10753  modqsubdir  10755  frec2uzisod  10769  uzennn  10798  iseqovex  10820  seqvalcd  10823  seq1g  10825  seqf  10826  seqovcd  10829  seqclg  10834  seqm1g  10836  seq3shft2  10843  seqshft2g  10844  monoord  10847  iseqf1olemnab  10863  seqf1oglem1  10881  seqf1og  10883  seqhomog  10892  seqfeq4g  10893  seq3distr  10894  expnegzap  10935  ltexp2a  10953  le2sq2  10977  bernneq  11022  expnlbnd2  11027  nn0ltexp2  11071  nn0opth2  11086  faclbnd  11103  bcval5  11125  hashcl  11144  hashen  11147  fihashdom  11167  hashunlem  11168  hashun  11169  hashxp  11191  hashmap  11192  fimaxq  11194  sseqn  11203  hashfibclem  11206  hashfibc  11207  zfz1isolem1  11212  zfz1iso  11213  seq3coll  11214  sswrd  11233  ccatw2s1p1g  11333  ccatw2s1p2  11334  ccat2s1fstg  11336  wrdind  11414  pfxccatin12lem1  11420  pfxccatin12lem3  11424  reuccatpfxs1lem  11438  cvg1nlemres  11670  cvg1n  11671  resqrexlemp1rp  11691  resqrexlemoverl  11706  resqrexlemex  11710  sqrtsq  11729  abslt  11773  absle  11774  abs3lem  11796  maxleastlt  11900  maxltsup  11903  fimaxre2  11912  negfi  11913  xrmaxleastlt  11941  xrmaxltsup  11943  xrmaxaddlem  11945  2clim  11986  climcn2  11994  addcn2  11995  mulcn2  11997  reccn2ap  11998  climge0  12010  climcau  12032  fzf1o  12061  summodclem2  12068  summodc  12069  zsumdc  12070  fsumf1o  12076  fisumss  12078  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  mptfzshft  12128  fsumrev  12129  fsummulc2  12134  fsumconst  12140  modfsummod  12144  fsumrelem  12157  binom  12170  cvgratnn  12217  mertenslemub  12220  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  fprodcl2lem  12291  fprodrev  12305  fprodconst  12306  fprodap0  12307  fprodrec  12315  fprodap0f  12322  fprodle  12326  fprodmodd  12327  efcllem  12345  tanaddaplem  12424  moddvds  12485  dvdsflip  12537  oexpneg  12563  nn0o  12593  fldivndvdslt  12623  bitsfi  12643  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlemeu  12703  dfgcd3  12706  dfgcd2  12710  dvdsmulgcd  12721  bezoutr  12728  nninfctlemfo  12736  lcmgcdlem  12774  coprmdvds2  12790  qredeu  12794  rpdvds  12796  cncongr1  12800  prmind2  12817  isprm5lem  12838  isprm6  12844  oddpwdclemdc  12870  nonsq  12904  hashdvds  12918  crth  12921  eulerthlemh  12928  prmdiveq  12933  hashgcdlem  12935  hashgcdeq  12937  nnnn0modprm0  12953  pclemub  12985  pceu  12993  pcmul  12999  pcqmul  13001  pcgcd1  13026  pc2dvds  13028  difsqpwdvds  13036  pcmpt  13041  prmpwdvds  13053  1arith  13065  mul4sq  13092  4sqlemafi  13093  4sqlemffi  13094  4sqexercise2  13097  ennnfonelemg  13154  ennnfonelemex  13165  ennnfonelemrnh  13167  ennnfonelemf1  13169  ennnfonelemrn  13170  ennnfonelemdm  13171  ennnfonelemim  13175  ennnfone  13176  ctinf  13181  ctiunctlemfo  13190  nninfdclemcl  13199  nninfdclemf  13200  nninfdclemp1  13201  unbendc  13205  isstruct2r  13223  setscom  13252  ercpbl  13544  opifismgmdc  13584  grpinvalem  13598  igsumvalx  13602  gsumfzval  13604  gsumval2  13610  sgrppropd  13626  prdssgrpd  13628  mndpropd  13653  issubmnd  13655  submnd0  13657  prdsmndd  13661  mhmf1o  13683  subsubm  13696  0mhm  13699  resmhm  13700  mhmco  13703  mhmima  13704  mhmeql  13705  gsumfzz  13708  gsumwsubmcl  13709  gsumfzcl  13712  grprcan  13750  grpinvid1  13765  grpinvid2  13766  grplcan  13775  grplmulf1o  13787  grpnpncan0  13809  dfgrp3mlem  13811  grplactcnv  13815  pwssub  13826  mulgval  13839  mulgfng  13841  mulgnngsum  13844  mulg1  13846  mulgnnp1  13847  mulgneg  13857  mulgnndir  13868  mulgdirlem  13870  mulgnn0ass  13875  mulgass  13876  subgmulg  13905  issubg4m  13910  subsubg  13914  subgintm  13915  isnsg3  13924  eqgcpbl  13945  ghmeql  13984  ghmnsgima  13985  ghmnsgpreima  13986  ghmf1  13990  ghmf1o  13992  conjghm  13993  qusghm  13999  ablpncan3  14034  invghm  14046  eqgabl  14047  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  rngpropd  14099  imasrng  14100  qusrng  14102  srglmhm  14137  srgrmhm  14138  ringpropd  14182  ringlghm  14205  ringrghm  14206  imasring  14208  qusring2  14210  opprrngbg  14222  dvdsrvald  14238  dvdsrd  14239  dvdsrex  14243  dvdsrtr  14246  unitpropdg  14293  rhmopp  14321  isnzr2  14329  issubrng2  14355  subrngintm  14357  subsubrng  14359  subrgintm  14388  subsubrg  14390  rhmpropd  14399  aprap  14432  lmodprop2d  14496  rmodislmod  14499  lssvacl  14513  lssvsubcl  14514  lssvscl  14523  islss3  14527  lss1d  14531  rnglidlmcl  14628  2idlcpblrng  14671  crngridl  14678  expghmap  14755  mulgghm2  14756  mulgrhm  14757  znf1o  14799  znleval  14801  znidom  14805  znidomb  14806  znunit  14807  psrbagcon  14826  mplsubgfilemcl  14854  iuncld  14980  ssnei2  15022  topssnei  15027  restopnb  15046  cnfval  15059  cnpfval  15060  iscnp4  15083  cnptopco  15087  cncnpi  15093  cncnp  15095  cnconst2  15098  cnrest2  15101  cnptoprest  15104  cnptoprest2  15105  cnpdis  15107  lmss  15111  lmtopcnp  15115  neitx  15133  txcnp  15136  txrest  15141  txdis1cn  15143  txlm  15144  cnmpt21  15156  imasnopn  15164  xmetres2  15244  blvalps  15253  blval  15254  elbl2ps  15257  elbl2  15258  blhalf  15273  blssexps  15294  blssex  15295  ssblex  15296  blin2  15297  bdmetval  15365  xmetxp  15372  xmettx  15375  metcnpi3  15382  txmetcnp  15383  addcncntoplem  15426  fsumcncntop  15432  elcncf2  15439  mulc1cncf  15454  cncfco  15456  cncfmet  15457  cncfmptc  15461  mulcncf  15473  dedekindeulemub  15483  dedekindeulemloc  15484  dedekindeulemlu  15486  dedekindeu  15488  dedekindicclemub  15492  dedekindicclemloc  15493  dedekindicclemlu  15495  dedekindicclemicc  15497  dedekindicc  15498  ivthinclemlopn  15501  ivthinclemuopn  15503  dich0  15517  limcimo  15530  cnplimccntop  15535  limccnp2lem  15541  limccnp2cntop  15542  dvfvalap  15546  dveflem  15591  plycolemc  15623  plyco  15624  plyrecj  15628  reeff1olem  15636  reeff1oleme  15637  eflt  15640  sin0pilem2  15647  pilem3  15648  ioocosf1o  15719  cxplt  15781  cxple  15782  cxplt3  15785  apcxp2  15804  rprelogbmul  15820  rprelogbdiv  15822  logbgt0b  15831  logbgcd1irrap  15835  pellexlem3  15847  mpodvdsmulf1o  15858  fsumdvdsmul  15859  lgsdir2lem5  15905  lgsdi  15910  lgsne0  15911  gausslemma2dlem1f1o  15933  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem2  15955  lgsquad2  15956  2sqlem6  15993  2sqlem8  15996  2sqlem9  15997  2sqlem10  15998  upgredg  16139  usgredg4  16210  uspgredg2vlem  16215  usgr1eop  16240  upgrspanop  16278  umgrspanop  16279  usgrspanop  16280  vtxedgfi  16284  vtxlpfi  16285  iswlkg  16324  upgriswlkdc  16355  upgr2wlkdc  16372  clwwlkccatlem  16395  clwwlknonex2e  16435  nnti  16766  pwtrufal  16771  pwf1oexmid  16773  sssneq  16776  qdencn  16807  cvgcmp2n  16817  trilpolemlt1  16825  trirec0  16828  qdiff  16833  redc0  16842  reap0  16843  cndcap  16844  nconstwlpolemgt0  16850  neap0mkv  16855  supfz  16857  inffz  16858  gfsumval  16862  gfsumz  16869  gfsumcl  16870