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  6577  tfrcldm  6638  tfrcl  6639  nntr2  6780  swoer  6839  erinxp  6887  ecopovsymg  6912  th3qlem1  6915  f1imaen2g  7084  pw2f1odclem  7138  mapdom1g  7151  fict  7174  fidifsnen  7176  dif1enen  7188  fiunsnnn  7189  fisbth  7191  findcard2d  7199  findcard2sd  7200  diffifi  7202  ac6sfi  7206  fimax2gtri  7210  nnwetri  7227  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  fisseneq  7246  ssfirab  7248  exmidssfi  7250  fidcenumlemrk  7276  fidcenumlemr  7277  sbthlemi6  7284  sbthlemi8  7286  isbth  7289  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  9744  suprzclex  9755  qapne  10055  xrlelttr  10225  xrltletr  10226  xrre3  10241  xrrege0  10244  xaddge0  10297  xle2add  10298  xlt2add  10299  fzass4  10485  fzrev  10508  elfz1b  10514  eluzgtdifelfzo  10632  fzocatel  10634  zsupcllemstep  10679  zsupcllemex  10680  zssinfcl  10682  infssfzcldc  10686  infssfzledc  10687  suprzubdc  10688  exbtwnzlemex  10701  rebtwn2z  10706  modqid  10807  modqcyc  10817  modqaddabs  10820  modqaddmod  10821  mulqaddmodid  10822  modqadd2mod  10832  modqltm1p1mod  10834  modqsubmod  10840  modqsubmodmod  10841  modaddmodup  10845  modqmulmod  10847  modqmulmodr  10848  modqaddmulmod  10849  modqsubdir  10851  frec2uzisod  10865  uzennn  10894  iseqovex  10916  seqvalcd  10919  seq1g  10921  seqf  10922  seqovcd  10925  seqclg  10930  seqm1g  10932  seq3shft2  10939  seqshft2g  10940  monoord  10943  iseqf1olemnab  10959  seqf1oglem1  10977  seqf1og  10979  seqhomog  10988  seqfeq4g  10989  seq3distr  10990  expnegzap  11031  ltexp2a  11049  le2sq2  11073  bernneq  11119  expnlbnd2  11124  nn0ltexp2  11169  nn0opth2  11184  faclbnd  11201  bcval5  11223  hashcl  11242  hashen  11245  fihashdom  11265  hashunlem  11266  hashun  11267  hashxp  11289  hashmap  11290  fimaxq  11292  sseqn  11301  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  zfz1isolem1  11314  zfz1iso  11315  seq3coll  11316  sswrd  11335  ccatw2s1p1g  11435  ccatw2s1p2  11436  ccat2s1fstg  11438  wrdind  11516  pfxccatin12lem1  11522  pfxccatin12lem3  11526  reuccatpfxs1lem  11540  cvg1nlemres  11773  cvg1n  11774  resqrexlemp1rp  11794  resqrexlemoverl  11809  resqrexlemex  11813  sqrtsq  11832  abslt  11877  absle  11878  abs3lem  11900  maxleastlt  12004  maxltsup  12007  fimaxre2  12016  negfi  12017  fiidxsupcl  12018  xrmaxleastlt  12047  xrmaxltsup  12049  xrmaxaddlem  12051  2clim  12092  climcn2  12100  addcn2  12101  mulcn2  12103  reccn2ap  12104  climge0  12116  climcau  12138  fzf1o  12167  summodclem2  12174  summodc  12175  zsumdc  12176  fsumf1o  12182  fisumss  12184  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  mptfzshft  12234  fsumrev  12235  fsummulc2  12240  fsumconst  12246  modfsummod  12250  fsumrelem  12263  binom  12276  cvgratnn  12323  mertenslemub  12326  prodmodclem2  12369  prodmodc  12370  zproddc  12371  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  fprodcl2lem  12397  fprodrev  12411  fprodconst  12412  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  fprodmodd  12433  efcllem  12451  tanaddaplem  12530  moddvds  12591  dvdsflip  12643  oexpneg  12669  nn0o  12699  fldivndvdslt  12729  bitsfi  12749  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemeu  12809  dfgcd3  12812  dfgcd2  12816  dvdsmulgcd  12827  bezoutr  12834  nninfctlemfo  12842  lcmgcdlem  12880  coprmdvds2  12896  qredeu  12900  rpdvds  12902  cncongr1  12906  prmind2  12923  isprm5lem  12945  isprm6  12951  nnmaxpwlemparts  12977  nnmaxpw  12978  nonsq  13012  nn0sqdcq  13013  sqrtrirr  13014  hashdvds  13028  crth  13031  eulerthlemh  13038  prmdiveq  13043  hashgcdlem  13045  hashgcdeq  13047  nnnn0modprm0  13063  pclemub  13095  pceu  13103  pcmul  13109  pcqmul  13111  pcgcd1  13136  pc2dvds  13138  difsqpwdvds  13146  pcmpt  13151  prmpwdvds  13163  1arith  13175  mul4sq  13202  4sqlemafi  13203  4sqlemffi  13204  4sqexercise2  13207  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemg  13352  ennnfonelemex  13363  ennnfonelemrnh  13365  ennnfonelemf1  13367  ennnfonelemrn  13368  ennnfonelemdm  13369  ennnfonelemim  13373  ennnfone  13374  ctinf  13379  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdclemf  13398  nninfdclemp1  13399  unbendc  13403  isstruct2r  13421  setscom  13450  ercpbl  13711  opifismgmdc  13750  grpinvalem  13764  gzsumvalx  13768  gzsumfzval  13770  gzsumval2  13773  sgrppropd  13787  mndpropd  13812  issubmnd  13814  submnd0  13816  mhmf1o  13836  subsubm  13849  0mhm  13852  resmhm  13853  mhmco  13856  mhmima  13857  mhmeql  13858  gzsumwsubmcl  13860  gzsumcl  13863  grprcan  13901  grpinvid1  13916  grpinvid2  13917  grplcan  13926  grplmulf1o  13938  grpnpncan0  13960  dfgrp3mlem  13962  grplactcnv  13966  mulgval  13984  mulgfng  13986  mulgnngzsum  13989  mulg1  13991  mulgnnp1  13992  mulgneg  14002  mulgnndir  14013  mulgdirlem  14015  mulgnn0ass  14020  mulgass  14021  subgmulg  14050  issubg4m  14055  subsubg  14059  subgintm  14060  isnsg3  14069  eqgcpbl  14090  ghmeql  14129  ghmnsgima  14130  ghmnsgpreima  14131  ghmf1  14135  ghmf1o  14137  conjghm  14138  qusghm  14144  cntzsgrpcl  14167  cntzsubm  14170  cntrsubgnsg  14175  cmnsubm  14202  ablpncan3  14211  invghm  14223  eqgabl  14224  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gsumvalfi  14242  gsumzfi  14248  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumresfi  14263  gsumconstcmn  14266  gsum2dfilem2  14272  gsum2d2fi  14274  prdssgrpd  14298  prdsmndd  14301  pwssub  14323  rngpropd  14361  imasrng  14362  qusrng  14364  srglmhm  14404  srgrmhm  14405  ringpropd  14450  ringlghm  14473  ringrghm  14474  imasring  14478  qusring2  14480  opprrngbg  14492  dvdsrvald  14509  dvdsrd  14510  dvdsrex  14514  dvdsrtr  14517  unitpropdg  14564  rhmopp  14592  isnzr2  14600  issubrng2  14627  subrngintm  14629  subsubrng  14631  subrgintm  14660  subsubrg  14662  rhmpropd  14671  ringunitap  14702  aprap  14707  drngunitap  14717  lmodprop2d  14794  rmodislmod  14797  lssvacl  14811  lssvsubcl  14812  lssvscl  14821  islss3  14825  lss1d  14829  rnglidlmcl  14926  2idlcpblrng  14969  crngridl  14976  gsumfsum  15032  expghmap  15051  mulgghm2  15052  mulgrhm  15053  znf1o  15095  znleval  15097  znidom  15101  znidomb  15102  znunit  15103  asclghm  15134  issubassa2  15144  assamulgscmlem2  15151  psrbagcon  15171  psrbaglefifi  15172  gsumbagdiaglem  15175  mplsubgfilemcl  15215  iuncld  15341  ssnei2  15383  topssnei  15388  restopnb  15407  cnfval  15420  cnpfval  15421  iscnp4  15444  cnptopco  15448  cncnpi  15454  cncnp  15456  cnconst2  15459  cnrest2  15462  cnptoprest  15465  cnptoprest2  15466  cnpdis  15468  lmss  15472  lmtopcnp  15476  neitx  15494  txcnp  15497  txrest  15502  txdis1cn  15504  txlm  15505  cnmpt21  15517  imasnopn  15525  xmetres2  15605  blvalps  15614  blval  15615  elbl2ps  15618  elbl2  15619  blhalf  15634  blssexps  15655  blssex  15656  ssblex  15657  blin2  15658  bdmetval  15726  xmetxp  15733  xmettx  15736  metcnpi3  15743  txmetcnp  15744  addcncntoplem  15787  fsumcncntop  15793  elcncf2  15800  mulc1cncf  15815  cncfco  15817  cncfmet  15818  cncfmptc  15822  mulcncf  15834  dedekindeulemub  15844  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeu  15849  dedekindicclemub  15853  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicclemicc  15858  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemuopn  15864  dich0  15878  limcimo  15891  cnplimccntop  15896  limccnp2lem  15902  limccnp2cntop  15903  dvfvalap  15907  dveflem  15952  plycolemc  15984  plyco  15985  plyrecj  15989  reeff1olem  15997  reeff1oleme  15998  eflt  16001  sin0pilem2  16009  pilem3  16010  ioocosf1o  16082  logdivlt  16124  logdivle  16125  rpcxpmul2z  16148  cxplt  16151  cxple  16152  cxplt3  16155  apcxp2  16174  rprelogbmul  16191  rprelogbdiv  16193  logbgt0b  16202  logbgcd1irrap  16206  zprmlogbap  16218  pellexlem3  16231  ppinprm  16260  chtnprm  16262  mpodvdsmulf1o  16284  fsumdvdsmul  16285  chtublem  16295  bposlem3  16313  lgsdir2lem5  16356  lgsdi  16361  lgsne0  16362  gausslemma2dlem1f1o  16384  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad2lem2  16406  lgsquad2  16407  2sqlem6  16444  2sqlem8  16447  2sqlem9  16448  2sqlem10  16449  upgredg  16590  usgredg4  16661  uspgredg2vlem  16666  usgr1eop  16691  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  vtxedgfi  16735  vtxlpfi  16736  iswlkg  16775  upgriswlkdc  16806  upgr2wlkdc  16823  clwwlkccatlem  16846  clwwlknonex2e  16886  nnti  17227  pwtrufal  17232  pwf1oexmid  17234  sssneq  17237  qdencn  17278  cvgcmp2n  17288  trilpolemlt1  17297  trirec0  17300  qdiff  17305  redc0  17314  reap0  17315  cndcap  17316  nconstwlpolemgt0  17321  neap0mkv  17326  supfz  17328  inffz  17329