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  989  simp1rr  1089  simp2rr  1093  simp3rr  1097  elpr2elpr  3859  invdisjrab  4082  disjiun  4083  reg2exmidlema  4632  reg3exmidlemwe  4677  nnsucpred  4715  iotam  5318  fvmptt  5738  fcof1  5924  fliftfun  5937  isotr  5957  riotass2  6000  acexmidlemab  6012  ovmpodf  6153  fnmpoovd  6380  1stconst  6386  2ndconst  6387  cnvf1olem  6389  f1od2  6400  smoiso  6468  tfrcldm  6529  tfrcl  6530  nntr2  6671  swoer  6730  erinxp  6778  ecopovsymg  6803  th3qlem1  6806  f1imaen2g  6967  pw2f1odclem  7020  mapdom1g  7033  fict  7055  fidifsnen  7057  dif1enen  7069  fiunsnnn  7070  fisbth  7072  findcard2d  7080  findcard2sd  7081  diffifi  7083  ac6sfi  7087  fimax2gtri  7091  nnwetri  7108  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  ssfirab  7129  exmidssfi  7131  fidcenumlemrk  7153  fidcenumlemr  7154  sbthlemi6  7161  sbthlemi8  7163  isbth  7166  fiuni  7177  supmaxti  7203  infminti  7226  ordiso2  7234  eldju2ndl  7271  eldju2ndr  7272  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctmlemr  7307  ctssdccl  7310  nninfninc  7322  fodjum  7345  fodju0  7346  omniwomnimkv  7366  exmidfodomrlemrALT  7414  acfun  7422  exmidaclem  7423  netap  7473  exmidmotap  7480  ccfunen  7483  cc1  7484  cc2lem  7485  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  distrnqg  7607  enq0sym  7652  enq0tr  7654  distrnq0  7679  prarloclem3  7717  genplt2i  7730  addlocpr  7756  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltaprg  7839  prplnqu  7840  addextpr  7841  recexprlemdisj  7850  recexprlemloc  7851  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  archpr  7863  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemdisj  7922  caucvgprprlemloc  7923  caucvgprprlemaddq  7928  suplocexprlemrl  7937  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  recexgt0sr  7993  mulgt0sr  7998  prsrriota  8008  suplocsrlem  8028  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axmulcom  8091  rereceu  8109  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  lelttr  8268  ltletr  8269  addcan  8359  addcan2  8360  addsub4  8422  ltadd2  8599  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  eqord1  8663  rereim  8766  apreap  8767  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  apneg  8791  mulext1  8792  mulext  8794  ltleap  8812  aprcl  8826  mulap0  8834  mulcanapd  8841  recapb  8851  rec11ap  8890  rec11rap  8891  divdivdivap  8893  ddcanap  8906  divadddivap  8907  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  lerec2  9069  ledivp1  9083  mulle0r  9124  nn0ge0div  9567  suprzclex  9578  qapne  9873  xrlelttr  10041  xrltletr  10042  xrre3  10057  xrrege0  10060  xaddge0  10113  xle2add  10114  xlt2add  10115  fzass4  10297  fzrev  10319  elfz1b  10325  eluzgtdifelfzo  10443  fzocatel  10445  zsupcllemstep  10490  zsupcllemex  10491  zssinfcl  10493  suprzubdc  10497  exbtwnzlemex  10510  rebtwn2z  10515  modqid  10612  modqcyc  10622  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqadd2mod  10637  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modaddmodup  10650  modqmulmod  10652  modqmulmodr  10653  modqaddmulmod  10654  modqsubdir  10656  frec2uzisod  10670  uzennn  10699  iseqovex  10721  seqvalcd  10724  seq1g  10726  seqf  10727  seqovcd  10730  seqclg  10735  seqm1g  10737  seq3shft2  10744  seqshft2g  10745  monoord  10748  iseqf1olemnab  10764  seqf1oglem1  10782  seqf1og  10784  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  expnegzap  10836  ltexp2a  10854  le2sq2  10878  bernneq  10923  expnlbnd2  10928  nn0ltexp2  10972  nn0opth2  10987  faclbnd  11004  bcval5  11026  hashcl  11044  hashen  11047  fihashdom  11067  hashunlem  11068  hashun  11069  hashxp  11091  fimaxq  11092  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  sswrd  11126  ccatw2s1p1g  11226  ccatw2s1p2  11227  ccat2s1fstg  11229  wrdind  11307  pfxccatin12lem1  11313  pfxccatin12lem3  11317  reuccatpfxs1lem  11331  cvg1nlemres  11550  cvg1n  11551  resqrexlemp1rp  11571  resqrexlemoverl  11586  resqrexlemex  11590  sqrtsq  11609  abslt  11653  absle  11654  abs3lem  11676  maxleastlt  11780  maxltsup  11783  fimaxre2  11792  negfi  11793  xrmaxleastlt  11821  xrmaxltsup  11823  xrmaxaddlem  11825  2clim  11866  climcn2  11874  addcn2  11875  mulcn2  11877  reccn2ap  11878  climge0  11890  climcau  11912  fzf1o  11941  summodclem2  11948  summodc  11949  zsumdc  11950  fsumf1o  11956  fisumss  11958  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  mptfzshft  12008  fsumrev  12009  fsummulc2  12014  fsumconst  12020  modfsummod  12024  fsumrelem  12037  binom  12050  cvgratnn  12097  mertenslemub  12100  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodf1o  12154  fprodssdc  12156  fprodmul  12157  fprodcl2lem  12171  fprodrev  12185  fprodconst  12186  fprodap0  12187  fprodrec  12195  fprodap0f  12202  fprodle  12206  fprodmodd  12207  efcllem  12225  tanaddaplem  12304  moddvds  12365  dvdsflip  12417  oexpneg  12443  nn0o  12473  fldivndvdslt  12503  bitsfi  12523  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemeu  12583  dfgcd3  12586  dfgcd2  12590  dvdsmulgcd  12601  bezoutr  12608  nninfctlemfo  12616  lcmgcdlem  12654  coprmdvds2  12670  qredeu  12674  rpdvds  12676  cncongr1  12680  prmind2  12697  isprm5lem  12718  isprm6  12724  oddpwdclemdc  12750  nonsq  12784  hashdvds  12798  crth  12801  eulerthlemh  12808  prmdiveq  12813  hashgcdlem  12815  hashgcdeq  12817  nnnn0modprm0  12833  pclemub  12865  pceu  12873  pcmul  12879  pcqmul  12881  pcgcd1  12906  pc2dvds  12908  difsqpwdvds  12916  pcmpt  12921  prmpwdvds  12933  1arith  12945  mul4sq  12972  4sqlemafi  12973  4sqlemffi  12974  4sqexercise2  12977  ennnfonelemg  13029  ennnfonelemex  13040  ennnfonelemrnh  13042  ennnfonelemf1  13044  ennnfonelemrn  13045  ennnfonelemdm  13046  ennnfonelemim  13050  ennnfone  13051  ctinf  13056  ctiunctlemfo  13065  nninfdclemcl  13074  nninfdclemf  13075  nninfdclemp1  13076  unbendc  13080  isstruct2r  13098  setscom  13127  ercpbl  13419  opifismgmdc  13459  grpinvalem  13473  igsumvalx  13477  gsumfzval  13479  gsumval2  13485  sgrppropd  13501  prdssgrpd  13503  mndpropd  13528  issubmnd  13530  submnd0  13532  prdsmndd  13536  mhmf1o  13558  subsubm  13571  0mhm  13574  resmhm  13575  mhmco  13578  mhmima  13579  mhmeql  13580  gsumfzz  13583  gsumwsubmcl  13584  gsumfzcl  13587  grprcan  13625  grpinvid1  13640  grpinvid2  13641  grplcan  13650  grplmulf1o  13662  grpnpncan0  13684  dfgrp3mlem  13686  grplactcnv  13690  pwssub  13701  mulgval  13714  mulgfng  13716  mulgnngsum  13719  mulg1  13721  mulgnnp1  13722  mulgneg  13732  mulgnndir  13743  mulgdirlem  13745  mulgnn0ass  13750  mulgass  13751  subgmulg  13780  issubg4m  13785  subsubg  13789  subgintm  13790  isnsg3  13799  eqgcpbl  13820  ghmeql  13859  ghmnsgima  13860  ghmnsgpreima  13861  ghmf1  13865  ghmf1o  13867  conjghm  13868  qusghm  13874  ablpncan3  13909  invghm  13921  eqgabl  13922  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  rngpropd  13974  imasrng  13975  qusrng  13977  srglmhm  14012  srgrmhm  14013  ringpropd  14057  ringlghm  14080  ringrghm  14081  imasring  14083  qusring2  14085  opprrngbg  14097  dvdsrvald  14113  dvdsrd  14114  dvdsrex  14118  dvdsrtr  14121  unitpropdg  14168  rhmopp  14196  isnzr2  14204  issubrng2  14230  subrngintm  14232  subsubrng  14234  subrgintm  14263  subsubrg  14265  rhmpropd  14274  aprap  14306  lmodprop2d  14368  rmodislmod  14371  lssvacl  14385  lssvsubcl  14386  lssvscl  14395  islss3  14399  lss1d  14403  rnglidlmcl  14500  2idlcpblrng  14543  crngridl  14550  expghmap  14627  mulgghm2  14628  mulgrhm  14629  znf1o  14671  znleval  14673  znidom  14677  znidomb  14678  znunit  14679  mplsubgfilemcl  14719  iuncld  14845  ssnei2  14887  topssnei  14892  restopnb  14911  cnfval  14924  cnpfval  14925  iscnp4  14948  cnptopco  14952  cncnpi  14958  cncnp  14960  cnconst2  14963  cnrest2  14966  cnptoprest  14969  cnptoprest2  14970  cnpdis  14972  lmss  14976  lmtopcnp  14980  neitx  14998  txcnp  15001  txrest  15006  txdis1cn  15008  txlm  15009  cnmpt21  15021  imasnopn  15029  xmetres2  15109  blvalps  15118  blval  15119  elbl2ps  15122  elbl2  15123  blhalf  15138  blssexps  15159  blssex  15160  ssblex  15161  blin2  15162  bdmetval  15230  xmetxp  15237  xmettx  15240  metcnpi3  15247  txmetcnp  15248  addcncntoplem  15291  fsumcncntop  15297  elcncf2  15304  mulc1cncf  15319  cncfco  15321  cncfmet  15322  cncfmptc  15326  mulcncf  15338  dedekindeulemub  15348  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeu  15353  dedekindicclemub  15357  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicclemicc  15362  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  dich0  15382  limcimo  15395  cnplimccntop  15400  limccnp2lem  15406  limccnp2cntop  15407  dvfvalap  15411  dveflem  15456  plycolemc  15488  plyco  15489  plyrecj  15493  reeff1olem  15501  reeff1oleme  15502  eflt  15505  sin0pilem2  15512  pilem3  15513  ioocosf1o  15584  cxplt  15646  cxple  15647  cxplt3  15650  apcxp2  15669  rprelogbmul  15685  rprelogbdiv  15687  logbgt0b  15696  logbgcd1irrap  15700  mpodvdsmulf1o  15720  fsumdvdsmul  15721  lgsdir2lem5  15767  lgsdi  15772  lgsne0  15773  gausslemma2dlem1f1o  15795  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem2  15817  lgsquad2  15818  2sqlem6  15855  2sqlem8  15858  2sqlem9  15859  2sqlem10  15860  upgredg  16001  usgredg4  16072  uspgredg2vlem  16077  usgr1eop  16102  upgrspanop  16140  umgrspanop  16141  usgrspanop  16142  vtxedgfi  16146  vtxlpfi  16147  iswlkg  16186  upgriswlkdc  16217  upgr2wlkdc  16234  clwwlkccatlem  16257  clwwlknonex2e  16297  nnti  16617  pwtrufal  16624  pwf1oexmid  16626  sssneq  16629  qdencn  16657  cvgcmp2n  16663  trilpolemlt1  16671  trirec0  16674  redc0  16687  reap0  16688  cndcap  16689  nconstwlpolemgt0  16694  neap0mkv  16699  supfz  16701  inffz  16702  gfsumval  16706  gfsumcl  16713