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  4683  reg3exmidlemwe  4728  nnsucpred  4766  iotam  5372  fvmptt  5800  fcof1  5992  fliftfun  6005  isotr  6025  riotass2  6070  acexmidlemab  6082  ovmpodf  6223  fnmpoovd  6455  1stconst  6461  2ndconst  6462  cnvf1olem  6464  f1od2  6475  suppcofn  6510  smoiso  6578  tfrcldm  6639  tfrcl  6640  nntr2  6781  swoer  6840  erinxp  6888  ecopovsymg  6913  th3qlem1  6916  f1imaen2g  7086  pw2f1odclem  7140  mapdom1g  7153  fict  7176  fidifsnen  7178  dif1enen  7190  fiunsnnn  7191  fisbth  7193  findcard2d  7201  findcard2sd  7202  diffifi  7204  ac6sfi  7208  fimax2gtri  7212  nnwetri  7229  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  fisseneq  7248  ssfirab  7250  exmidssfi  7252  fidcenumlemrk  7278  fidcenumlemr  7279  sbthlemi6  7286  sbthlemi8  7288  isbth  7291  fiuni  7317  supmaxti  7350  infminti  7373  ordiso2  7381  eldju2ndl  7418  eldju2ndr  7419  omp1eomlem  7440  difinfsnlem  7445  difinfinf  7447  ctmlemr  7454  ctssdccl  7457  nninfninc  7469  fodjum  7492  fodju0  7493  omniwomnimkv  7513  exmidfodomrlemrALT  7561  acfun  7569  exmidaclem  7570  netap  7626  exmidmotap  7633  ccfunen  7636  cc1  7637  cc2lem  7638  dfplpq2  7727  dfmpq2  7728  mulpipqqs  7746  distrnqg  7760  enq0sym  7805  enq0tr  7807  distrnq0  7832  prarloclem3  7870  genplt2i  7883  addlocpr  7909  prmuloc  7939  distrlem1prl  7955  distrlem1pru  7956  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltaprg  7992  prplnqu  7993  addextpr  7994  recexprlemdisj  8003  recexprlemloc  8004  aptiprleml  8012  aptiprlemu  8013  ltmprr  8015  archpr  8016  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlemlim  8034  caucvgprlemnkj  8039  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemdisj  8075  caucvgprprlemloc  8076  caucvgprprlemaddq  8081  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  recexgt0sr  8146  mulgt0sr  8151  prsrriota  8161  suplocsrlem  8181  addcnsr  8207  mulcnsr  8208  mulcnsrec  8216  axmulcom  8244  rereceu  8262  axarch  8264  axcaucvglemres  8272  axpre-suploclemres  8274  lelttr  8420  ltletr  8421  addcan  8513  addcan2  8514  addsub4  8576  ltadd2  8754  le2add  8779  lt2add  8780  lt2sub  8795  le2sub  8796  eqord1  8818  rereim  8922  apreap  8923  apreim  8939  mulreim  8940  apcotr  8943  apadd1  8944  addext  8946  apneg  8947  mulext1  8948  mulext  8950  ltleap  8968  aprcl  8982  mulap0  8990  mulcanapd  8997  recapb  9009  rec11ap  9048  rec11rap  9049  divdivdivap  9051  ddcanap  9064  divadddivap  9065  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemulge11  9204  lt2mul2div  9217  ltrec  9221  lerec  9222  lerec2  9227  ledivp1  9241  mulle0r  9282  nn0ge0div  9742  suprzclex  9754  qapne  10054  xrlelttr  10224  xrltletr  10225  xrre3  10240  xrrege0  10243  xaddge0  10296  xle2add  10297  xlt2add  10298  fzass4  10484  fzrev  10507  elfz1b  10513  eluzgtdifelfzo  10631  fzocatel  10633  zsupcllemstep  10678  zsupcllemex  10679  zssinfcl  10681  infssfzcldc  10685  infssfzledc  10686  suprzubdc  10687  exbtwnzlemex  10700  rebtwn2z  10705  modqid  10806  modqcyc  10816  modqaddabs  10819  modqaddmod  10820  mulqaddmodid  10821  modqadd2mod  10831  modqltm1p1mod  10833  modqsubmod  10839  modqsubmodmod  10840  modaddmodup  10844  modqmulmod  10846  modqmulmodr  10847  modqaddmulmod  10848  modqsubdir  10850  frec2uzisod  10864  uzennn  10893  iseqovex  10915  seqvalcd  10918  seq1g  10920  seqf  10921  seqovcd  10924  seqclg  10929  seqm1g  10931  seq3shft2  10938  seqshft2g  10939  monoord  10942  iseqf1olemnab  10958  seqf1oglem1  10976  seqf1og  10978  seqhomog  10987  seqfeq4g  10988  seq3distr  10989  expnegzap  11030  ltexp2a  11048  le2sq2  11072  bernneq  11118  expnlbnd2  11123  nn0ltexp2  11168  nn0opth2  11183  faclbnd  11200  bcval5  11222  hashcl  11241  hashen  11244  fihashdom  11264  hashunlem  11265  hashun  11266  hashxp  11288  hashmap  11289  fimaxq  11291  sseqn  11300  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  hashf1  11308  zfz1isolem1  11313  zfz1iso  11314  seq3coll  11315  sswrd  11334  ccatw2s1p1g  11434  ccatw2s1p2  11435  ccat2s1fstg  11437  wrdind  11515  pfxccatin12lem1  11521  pfxccatin12lem3  11525  reuccatpfxs1lem  11539  cvg1nlemres  11772  cvg1n  11773  resqrexlemp1rp  11793  resqrexlemoverl  11808  resqrexlemex  11812  sqrtsq  11831  abslt  11876  absle  11877  abs3lem  11899  maxleastlt  12003  maxltsup  12006  fimaxre2  12015  negfi  12016  fiidxsupcl  12017  xrmaxleastlt  12046  xrmaxltsup  12048  xrmaxaddlem  12050  2clim  12091  climcn2  12099  addcn2  12100  mulcn2  12102  reccn2ap  12103  climge0  12115  climcau  12137  fzf1o  12166  summodclem2  12173  summodc  12174  zsumdc  12175  fsumf1o  12181  fisumss  12183  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  mptfzshft  12233  fsumrev  12234  fsummulc2  12239  fsumconst  12245  modfsummod  12249  fsumrelem  12262  binom  12275  cvgratnn  12322  mertenslemub  12325  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  fprodcl2lem  12396  fprodrev  12410  fprodconst  12411  fprodap0  12412  fprodrec  12420  fprodap0f  12427  fprodle  12431  fprodmodd  12432  efcllem  12450  tanaddaplem  12529  moddvds  12590  dvdsflip  12642  oexpneg  12668  nn0o  12698  fldivndvdslt  12728  bitsfi  12748  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemeu  12808  dfgcd3  12811  dfgcd2  12815  dvdsmulgcd  12826  bezoutr  12833  nninfctlemfo  12841  lcmgcdlem  12879  coprmdvds2  12895  qredeu  12899  rpdvds  12901  cncongr1  12905  prmind2  12922  isprm5lem  12944  isprm6  12950  nnmaxpwlemparts  12976  nnmaxpw  12977  nonsq  13011  nn0sqdcq  13012  sqrtrirr  13013  hashdvds  13027  crth  13030  eulerthlemh  13037  prmdiveq  13042  hashgcdlem  13044  hashgcdeq  13046  nnnn0modprm0  13062  pclemub  13094  pceu  13102  pcmul  13108  pcqmul  13110  pcgcd1  13135  pc2dvds  13137  difsqpwdvds  13145  pcmpt  13150  prmpwdvds  13162  1arith  13174  mul4sq  13201  4sqlemafi  13202  4sqlemffi  13203  4sqexercise2  13206  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemg  13351  ennnfonelemex  13362  ennnfonelemrnh  13364  ennnfonelemf1  13366  ennnfonelemrn  13367  ennnfonelemdm  13368  ennnfonelemim  13372  ennnfone  13373  ctinf  13378  ctiunctlemfo  13387  nninfdclemcl  13396  nninfdclemf  13397  nninfdclemp1  13398  unbendc  13402  isstruct2r  13420  setscom  13449  ercpbl  13710  opifismgmdc  13749  grpinvalem  13763  gzsumvalx  13767  gzsumfzval  13769  gzsumval2  13772  sgrppropd  13786  mndpropd  13811  issubmnd  13813  submnd0  13815  mhmf1o  13835  subsubm  13848  0mhm  13851  resmhm  13852  mhmco  13855  mhmima  13856  mhmeql  13857  gzsumwsubmcl  13859  gzsumcl  13862  grprcan  13900  grpinvid1  13915  grpinvid2  13916  grplcan  13925  grplmulf1o  13937  grpnpncan0  13959  dfgrp3mlem  13961  grplactcnv  13965  mulgval  13983  mulgfng  13985  mulgnngzsum  13988  mulg1  13990  mulgnnp1  13991  mulgneg  14001  mulgnndir  14012  mulgdirlem  14014  mulgnn0ass  14019  mulgass  14020  subgmulg  14049  issubg4m  14054  subsubg  14058  subgintm  14059  isnsg3  14068  eqgcpbl  14089  ghmeql  14128  ghmnsgima  14129  ghmnsgpreima  14130  ghmf1  14134  ghmf1o  14136  conjghm  14137  qusghm  14143  cntzsgrpcl  14166  cntzsubm  14169  cntrsubgnsg  14174  cmnsubm  14201  ablpncan3  14210  invghm  14222  eqgabl  14223  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gsumvalfi  14241  gsumzfi  14247  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumresfi  14262  gsumconstcmn  14265  gsum2dfilem2  14271  gsum2d2fi  14273  prdssgrpd  14297  prdsmndd  14300  pwssub  14322  rngpropd  14360  imasrng  14361  qusrng  14363  srglmhm  14403  srgrmhm  14404  ringpropd  14449  ringlghm  14472  ringrghm  14473  imasring  14477  qusring2  14479  opprrngbg  14491  dvdsrvald  14508  dvdsrd  14509  dvdsrex  14513  dvdsrtr  14516  unitpropdg  14563  rhmopp  14591  isnzr2  14599  issubrng2  14626  subrngintm  14628  subsubrng  14630  subrgintm  14659  subsubrg  14661  rhmpropd  14670  ringunitap  14701  aprap  14706  drngunitap  14716  lmodprop2d  14793  rmodislmod  14796  lssvacl  14810  lssvsubcl  14811  lssvscl  14820  islss3  14824  lss1d  14828  rnglidlmcl  14925  2idlcpblrng  14968  crngridl  14975  gsumfsum  15031  expghmap  15050  mulgghm2  15051  mulgrhm  15052  znf1o  15094  znleval  15096  znidom  15100  znidomb  15101  znunit  15102  asclghm  15133  issubassa2  15143  assamulgscmlem2  15150  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmax  15183  gsumbagdiaglem  15184  mvrclfi  15226  mplsubgfilemcl  15232  iuncld  15358  ssnei2  15400  topssnei  15405  restopnb  15424  cnfval  15437  cnpfval  15438  iscnp4  15461  cnptopco  15465  cncnpi  15471  cncnp  15473  cnconst2  15476  cnrest2  15479  cnptoprest  15482  cnptoprest2  15483  cnpdis  15485  lmss  15489  lmtopcnp  15493  neitx  15511  txcnp  15514  txrest  15519  txdis1cn  15521  txlm  15522  cnmpt21  15534  imasnopn  15542  xmetres2  15622  blvalps  15631  blval  15632  elbl2ps  15635  elbl2  15636  blhalf  15651  blssexps  15672  blssex  15673  ssblex  15674  blin2  15675  bdmetval  15743  xmetxp  15750  xmettx  15753  metcnpi3  15760  txmetcnp  15761  addcncntoplem  15804  fsumcncntop  15810  elcncf2  15817  mulc1cncf  15832  cncfco  15834  cncfmet  15835  cncfmptc  15839  mulcncf  15851  dedekindeulemub  15861  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeu  15866  dedekindicclemub  15870  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemicc  15875  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemuopn  15881  dich0  15895  limcimo  15908  cnplimccntop  15913  limccnp2lem  15919  limccnp2cntop  15920  dvfvalap  15924  dveflem  15969  plycolemc  16001  plyco  16002  plyrecj  16006  reeff1olem  16014  reeff1oleme  16015  eflt  16018  sin0pilem2  16026  pilem3  16027  ioocosf1o  16099  logdivlt  16141  logdivle  16142  rpcxpmul2z  16165  cxplt  16168  cxple  16169  cxplt3  16172  apcxp2  16191  rprelogbmul  16208  rprelogbdiv  16210  logbgt0b  16219  logbgcd1irrap  16223  zprmlogbap  16235  pellexlem3  16248  ppinprm  16277  chtnprm  16279  mpodvdsmulf1o  16301  fsumdvdsmul  16302  chtublem  16312  bposlem3  16330  lgsdir2lem5  16373  lgsdi  16378  lgsne0  16379  gausslemma2dlem1f1o  16401  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad2lem2  16423  lgsquad2  16424  2sqlem6  16461  2sqlem8  16464  2sqlem9  16465  2sqlem10  16466  upgredg  16607  usgredg4  16678  uspgredg2vlem  16683  usgr1eop  16708  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  vtxedgfi  16752  vtxlpfi  16753  iswlkg  16792  upgriswlkdc  16823  upgr2wlkdc  16840  clwwlkccatlem  16863  clwwlknonex2e  16903  nnti  17244  pwtrufal  17249  pwf1oexmid  17251  sssneq  17254  qdencn  17295  cvgcmp2n  17305  trilpolemlt1  17314  trirec0  17317  qdiff  17322  redc0  17331  reap0  17332  cndcap  17333  nconstwlpolemgt0  17338  neap0mkv  17343  supfz  17345  inffz  17346