Theorem simprr 531

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  987  simp1rr  1087  simp2rr  1091  simp3rr  1095  elpr2elpr  3853  invdisjrab  4076  disjiun  4077  reg2exmidlema  4625  reg3exmidlemwe  4670  nnsucpred  4708  iotam  5309  fvmptt  5725  fcof1  5906  fliftfun  5919  isotr  5939  riotass2  5982  acexmidlemab  5994  ovmpodf  6135  fnmpoovd  6359  1stconst  6365  2ndconst  6366  cnvf1olem  6368  f1od2  6379  smoiso  6446  tfrcldm  6507  tfrcl  6508  nntr2  6647  swoer  6706  erinxp  6754  ecopovsymg  6779  th3qlem1  6782  f1imaen2g  6943  pw2f1odclem  6991  mapdom1g  7004  fict  7026  fidifsnen  7028  dif1enen  7038  fiunsnnn  7039  fisbth  7041  findcard2d  7049  findcard2sd  7050  diffifi  7052  ac6sfi  7056  fimax2gtri  7059  nnwetri  7074  unsnfi  7077  unsnfidcex  7078  unsnfidcel  7079  fisseneq  7092  ssfirab  7094  fidcenumlemrk  7117  fidcenumlemr  7118  sbthlemi6  7125  sbthlemi8  7127  isbth  7130  fiuni  7141  supmaxti  7167  infminti  7190  ordiso2  7198  eldju2ndl  7235  eldju2ndr  7236  omp1eomlem  7257  difinfsnlem  7262  difinfinf  7264  ctmlemr  7271  ctssdccl  7274  nninfninc  7286  fodjum  7309  fodju0  7310  omniwomnimkv  7330  exmidfodomrlemrALT  7377  acfun  7385  exmidaclem  7386  netap  7436  exmidmotap  7443  ccfunen  7446  cc1  7447  cc2lem  7448  dfplpq2  7537  dfmpq2  7538  mulpipqqs  7556  distrnqg  7570  enq0sym  7615  enq0tr  7617  distrnq0  7642  prarloclem3  7680  genplt2i  7693  addlocpr  7719  prmuloc  7749  distrlem1prl  7765  distrlem1pru  7766  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemfl  7792  ltexprlemrl  7793  ltexprlemfu  7794  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  ltaprg  7802  prplnqu  7803  addextpr  7804  recexprlemdisj  7813  recexprlemloc  7814  aptiprleml  7822  aptiprlemu  7823  ltmprr  7825  archpr  7826  cauappcvgprlemopl  7829  cauappcvgprlemopu  7831  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlem1  7842  cauappcvgprlemlim  7844  caucvgprlemnkj  7849  caucvgprlemopl  7852  caucvgprlemopu  7854  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnjltk  7874  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemdisj  7885  caucvgprprlemloc  7886  caucvgprprlemaddq  7891  suplocexprlemrl  7900  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  recexgt0sr  7956  mulgt0sr  7961  prsrriota  7971  suplocsrlem  7991  addcnsr  8017  mulcnsr  8018  mulcnsrec  8026  axmulcom  8054  rereceu  8072  axarch  8074  axcaucvglemres  8082  axpre-suploclemres  8084  lelttr  8231  ltletr  8232  addcan  8322  addcan2  8323  addsub4  8385  ltadd2  8562  le2add  8587  lt2add  8588  lt2sub  8603  le2sub  8604  eqord1  8626  rereim  8729  apreap  8730  apreim  8746  mulreim  8747  apcotr  8750  apadd1  8751  addext  8753  apneg  8754  mulext1  8755  mulext  8757  ltleap  8775  aprcl  8789  mulap0  8797  mulcanapd  8804  recapb  8814  rec11ap  8853  rec11rap  8854  divdivdivap  8856  ddcanap  8869  divadddivap  8870  prodgt0gt0  8994  prodgt0  8995  prodge0  8997  lemulge11  9009  lt2mul2div  9022  ltrec  9026  lerec  9027  lerec2  9032  ledivp1  9046  mulle0r  9087  nn0ge0div  9530  suprzclex  9541  qapne  9830  xrlelttr  9998  xrltletr  9999  xrre3  10014  xrrege0  10017  xaddge0  10070  xle2add  10071  xlt2add  10072  fzass4  10254  fzrev  10276  elfz1b  10282  eluzgtdifelfzo  10398  fzocatel  10400  zsupcllemstep  10444  zsupcllemex  10445  zssinfcl  10447  suprzubdc  10451  exbtwnzlemex  10464  rebtwn2z  10469  modqid  10566  modqcyc  10576  modqaddabs  10579  modqaddmod  10580  mulqaddmodid  10581  modqadd2mod  10591  modqltm1p1mod  10593  modqsubmod  10599  modqsubmodmod  10600  modaddmodup  10604  modqmulmod  10606  modqmulmodr  10607  modqaddmulmod  10608  modqsubdir  10610  frec2uzisod  10624  uzennn  10653  iseqovex  10675  seqvalcd  10678  seq1g  10680  seqf  10681  seqovcd  10684  seqclg  10689  seqm1g  10691  seq3shft2  10698  seqshft2g  10699  monoord  10702  iseqf1olemnab  10718  seqf1oglem1  10736  seqf1og  10738  seqhomog  10747  seqfeq4g  10748  seq3distr  10749  expnegzap  10790  ltexp2a  10808  le2sq2  10832  bernneq  10877  expnlbnd2  10882  nn0ltexp2  10926  nn0opth2  10941  faclbnd  10958  bcval5  10980  hashcl  10998  hashen  11001  fihashdom  11020  hashunlem  11021  hashun  11022  hashxp  11043  fimaxq  11044  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  sswrd  11075  ccatw2s1p2  11171  wrdind  11249  pfxccatin12lem1  11255  pfxccatin12lem3  11259  reuccatpfxs1lem  11273  cvg1nlemres  11491  cvg1n  11492  resqrexlemp1rp  11512  resqrexlemoverl  11527  resqrexlemex  11531  sqrtsq  11550  abslt  11594  absle  11595  abs3lem  11617  maxleastlt  11721  maxltsup  11724  fimaxre2  11733  negfi  11734  xrmaxleastlt  11762  xrmaxltsup  11764  xrmaxaddlem  11766  2clim  11807  climcn2  11815  addcn2  11816  mulcn2  11818  reccn2ap  11819  climge0  11831  climcau  11853  summodclem2  11888  summodc  11889  zsumdc  11890  fsumf1o  11896  fisumss  11898  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  mptfzshft  11948  fsumrev  11949  fsummulc2  11954  fsumconst  11960  modfsummod  11964  fsumrelem  11977  binom  11990  cvgratnn  12037  mertenslemub  12040  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  fprodcl2lem  12111  fprodrev  12125  fprodconst  12126  fprodap0  12127  fprodrec  12135  fprodap0f  12142  fprodle  12146  fprodmodd  12147  efcllem  12165  tanaddaplem  12244  moddvds  12305  dvdsflip  12357  oexpneg  12383  nn0o  12413  fldivndvdslt  12443  bitsfi  12463  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemeu  12523  dfgcd3  12526  dfgcd2  12530  dvdsmulgcd  12541  bezoutr  12548  nninfctlemfo  12556  lcmgcdlem  12594  coprmdvds2  12610  qredeu  12614  rpdvds  12616  cncongr1  12620  prmind2  12637  isprm5lem  12658  isprm6  12664  oddpwdclemdc  12690  nonsq  12724  hashdvds  12738  crth  12741  eulerthlemh  12748  prmdiveq  12753  hashgcdlem  12755  hashgcdeq  12757  nnnn0modprm0  12773  pclemub  12805  pceu  12813  pcmul  12819  pcqmul  12821  pcgcd1  12846  pc2dvds  12848  difsqpwdvds  12856  pcmpt  12861  prmpwdvds  12873  1arith  12885  mul4sq  12912  4sqlemafi  12913  4sqlemffi  12914  4sqexercise2  12917  ennnfonelemg  12969  ennnfonelemex  12980  ennnfonelemrnh  12982  ennnfonelemf1  12984  ennnfonelemrn  12985  ennnfonelemdm  12986  ennnfonelemim  12990  ennnfone  12991  ctinf  12996  ctiunctlemfo  13005  nninfdclemcl  13014  nninfdclemf  13015  nninfdclemp1  13016  unbendc  13020  isstruct2r  13038  setscom  13067  ercpbl  13359  opifismgmdc  13399  grpinvalem  13413  igsumvalx  13417  gsumfzval  13419  gsumval2  13425  sgrppropd  13441  prdssgrpd  13443  mndpropd  13468  issubmnd  13470  submnd0  13472  prdsmndd  13476  mhmf1o  13498  subsubm  13511  0mhm  13514  resmhm  13515  mhmco  13518  mhmima  13519  mhmeql  13520  gsumfzz  13523  gsumwsubmcl  13524  gsumfzcl  13527  grprcan  13565  grpinvid1  13580  grpinvid2  13581  grplcan  13590  grplmulf1o  13602  grpnpncan0  13624  dfgrp3mlem  13626  grplactcnv  13630  pwssub  13641  mulgval  13654  mulgfng  13656  mulgnngsum  13659  mulg1  13661  mulgnnp1  13662  mulgneg  13672  mulgnndir  13683  mulgdirlem  13685  mulgnn0ass  13690  mulgass  13691  subgmulg  13720  issubg4m  13725  subsubg  13729  subgintm  13730  isnsg3  13739  eqgcpbl  13760  ghmeql  13799  ghmnsgima  13800  ghmnsgpreima  13801  ghmf1  13805  ghmf1o  13807  conjghm  13808  qusghm  13814  ablpncan3  13849  invghm  13861  eqgabl  13862  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  rngpropd  13913  imasrng  13914  qusrng  13916  srglmhm  13951  srgrmhm  13952  ringpropd  13996  ringlghm  14019  ringrghm  14020  imasring  14022  qusring2  14024  opprrngbg  14036  dvdsrvald  14051  dvdsrd  14052  dvdsrex  14056  dvdsrtr  14059  unitpropdg  14106  rhmopp  14134  isnzr2  14142  issubrng2  14168  subrngintm  14170  subsubrng  14172  subrgintm  14201  subsubrg  14203  rhmpropd  14212  aprap  14244  lmodprop2d  14306  rmodislmod  14309  lssvacl  14323  lssvsubcl  14324  lssvscl  14333  islss3  14337  lss1d  14341  rnglidlmcl  14438  2idlcpblrng  14481  crngridl  14488  expghmap  14565  mulgghm2  14566  mulgrhm  14567  znf1o  14609  znleval  14611  znidom  14615  znidomb  14616  znunit  14617  mplsubgfilemcl  14657  iuncld  14783  ssnei2  14825  topssnei  14830  restopnb  14849  cnfval  14862  cnpfval  14863  iscnp4  14886  cnptopco  14890  cncnpi  14896  cncnp  14898  cnconst2  14901  cnrest2  14904  cnptoprest  14907  cnptoprest2  14908  cnpdis  14910  lmss  14914  lmtopcnp  14918  neitx  14936  txcnp  14939  txrest  14944  txdis1cn  14946  txlm  14947  cnmpt21  14959  imasnopn  14967  xmetres2  15047  blvalps  15056  blval  15057  elbl2ps  15060  elbl2  15061  blhalf  15076  blssexps  15097  blssex  15098  ssblex  15099  blin2  15100  bdmetval  15168  xmetxp  15175  xmettx  15178  metcnpi3  15185  txmetcnp  15186  addcncntoplem  15229  fsumcncntop  15235  elcncf2  15242  mulc1cncf  15257  cncfco  15259  cncfmet  15260  cncfmptc  15264  mulcncf  15276  dedekindeulemub  15286  dedekindeulemloc  15287  dedekindeulemlu  15289  dedekindeu  15291  dedekindicclemub  15295  dedekindicclemloc  15296  dedekindicclemlu  15298  dedekindicclemicc  15300  dedekindicc  15301  ivthinclemlopn  15304  ivthinclemuopn  15306  dich0  15320  limcimo  15333  cnplimccntop  15338  limccnp2lem  15344  limccnp2cntop  15345  dvfvalap  15349  dveflem  15394  plycolemc  15426  plyco  15427  plyrecj  15431  reeff1olem  15439  reeff1oleme  15440  eflt  15443  sin0pilem2  15450  pilem3  15451  ioocosf1o  15522  cxplt  15584  cxple  15585  cxplt3  15588  apcxp2  15607  rprelogbmul  15623  rprelogbdiv  15625  logbgt0b  15634  logbgcd1irrap  15638  mpodvdsmulf1o  15658  fsumdvdsmul  15659  lgsdir2lem5  15705  lgsdi  15710  lgsne0  15711  gausslemma2dlem1f1o  15733  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad2lem2  15755  lgsquad2  15756  2sqlem6  15793  2sqlem8  15796  2sqlem9  15797  2sqlem10  15798  upgredg  15936  usgredg4  16007  uspgredg2vlem  16012  iswlkg  16032  nnti  16315  pwtrufal  16322  pwf1oexmid  16324  sssneq  16327  qdencn  16354  cvgcmp2n  16360  trilpolemlt1  16368  trirec0  16371  redc0  16384  reap0  16385  cndcap  16386  nconstwlpolemgt0  16391  neap0mkv  16396  supfz  16398  inffz  16399