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  11563  cvg1n  11564  resqrexlemp1rp  11584  resqrexlemoverl  11599  resqrexlemex  11603  sqrtsq  11622  abslt  11666  absle  11667  abs3lem  11689  maxleastlt  11793  maxltsup  11796  fimaxre2  11805  negfi  11806  xrmaxleastlt  11834  xrmaxltsup  11836  xrmaxaddlem  11838  2clim  11879  climcn2  11887  addcn2  11888  mulcn2  11890  reccn2ap  11891  climge0  11903  climcau  11925  fzf1o  11954  summodclem2  11961  summodc  11962  zsumdc  11963  fsumf1o  11969  fisumss  11971  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  mptfzshft  12021  fsumrev  12022  fsummulc2  12027  fsumconst  12033  modfsummod  12037  fsumrelem  12050  binom  12063  cvgratnn  12110  mertenslemub  12113  prodmodclem2  12156  prodmodc  12157  zproddc  12158  fprodf1o  12167  fprodssdc  12169  fprodmul  12170  fprodcl2lem  12184  fprodrev  12198  fprodconst  12199  fprodap0  12200  fprodrec  12208  fprodap0f  12215  fprodle  12219  fprodmodd  12220  efcllem  12238  tanaddaplem  12317  moddvds  12378  dvdsflip  12430  oexpneg  12456  nn0o  12486  fldivndvdslt  12516  bitsfi  12536  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemeu  12596  dfgcd3  12599  dfgcd2  12603  dvdsmulgcd  12614  bezoutr  12621  nninfctlemfo  12629  lcmgcdlem  12667  coprmdvds2  12683  qredeu  12687  rpdvds  12689  cncongr1  12693  prmind2  12710  isprm5lem  12731  isprm6  12737  oddpwdclemdc  12763  nonsq  12797  hashdvds  12811  crth  12814  eulerthlemh  12821  prmdiveq  12826  hashgcdlem  12828  hashgcdeq  12830  nnnn0modprm0  12846  pclemub  12878  pceu  12886  pcmul  12892  pcqmul  12894  pcgcd1  12919  pc2dvds  12921  difsqpwdvds  12929  pcmpt  12934  prmpwdvds  12946  1arith  12958  mul4sq  12985  4sqlemafi  12986  4sqlemffi  12987  4sqexercise2  12990  ennnfonelemg  13042  ennnfonelemex  13053  ennnfonelemrnh  13055  ennnfonelemf1  13057  ennnfonelemrn  13058  ennnfonelemdm  13059  ennnfonelemim  13063  ennnfone  13064  ctinf  13069  ctiunctlemfo  13078  nninfdclemcl  13087  nninfdclemf  13088  nninfdclemp1  13089  unbendc  13093  isstruct2r  13111  setscom  13140  ercpbl  13432  opifismgmdc  13472  grpinvalem  13486  igsumvalx  13490  gsumfzval  13492  gsumval2  13498  sgrppropd  13514  prdssgrpd  13516  mndpropd  13541  issubmnd  13543  submnd0  13545  prdsmndd  13549  mhmf1o  13571  subsubm  13584  0mhm  13587  resmhm  13588  mhmco  13591  mhmima  13592  mhmeql  13593  gsumfzz  13596  gsumwsubmcl  13597  gsumfzcl  13600  grprcan  13638  grpinvid1  13653  grpinvid2  13654  grplcan  13663  grplmulf1o  13675  grpnpncan0  13697  dfgrp3mlem  13699  grplactcnv  13703  pwssub  13714  mulgval  13727  mulgfng  13729  mulgnngsum  13732  mulg1  13734  mulgnnp1  13735  mulgneg  13745  mulgnndir  13756  mulgdirlem  13758  mulgnn0ass  13763  mulgass  13764  subgmulg  13793  issubg4m  13798  subsubg  13802  subgintm  13803  isnsg3  13812  eqgcpbl  13833  ghmeql  13872  ghmnsgima  13873  ghmnsgpreima  13874  ghmf1  13878  ghmf1o  13880  conjghm  13881  qusghm  13887  ablpncan3  13922  invghm  13934  eqgabl  13935  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  rngpropd  13987  imasrng  13988  qusrng  13990  srglmhm  14025  srgrmhm  14026  ringpropd  14070  ringlghm  14093  ringrghm  14094  imasring  14096  qusring2  14098  opprrngbg  14110  dvdsrvald  14126  dvdsrd  14127  dvdsrex  14131  dvdsrtr  14134  unitpropdg  14181  rhmopp  14209  isnzr2  14217  issubrng2  14243  subrngintm  14245  subsubrng  14247  subrgintm  14276  subsubrg  14278  rhmpropd  14287  aprap  14319  lmodprop2d  14381  rmodislmod  14384  lssvacl  14398  lssvsubcl  14399  lssvscl  14408  islss3  14412  lss1d  14416  rnglidlmcl  14513  2idlcpblrng  14556  crngridl  14563  expghmap  14640  mulgghm2  14641  mulgrhm  14642  znf1o  14684  znleval  14686  znidom  14690  znidomb  14691  znunit  14692  mplsubgfilemcl  14732  iuncld  14858  ssnei2  14900  topssnei  14905  restopnb  14924  cnfval  14937  cnpfval  14938  iscnp4  14961  cnptopco  14965  cncnpi  14971  cncnp  14973  cnconst2  14976  cnrest2  14979  cnptoprest  14982  cnptoprest2  14983  cnpdis  14985  lmss  14989  lmtopcnp  14993  neitx  15011  txcnp  15014  txrest  15019  txdis1cn  15021  txlm  15022  cnmpt21  15034  imasnopn  15042  xmetres2  15122  blvalps  15131  blval  15132  elbl2ps  15135  elbl2  15136  blhalf  15151  blssexps  15172  blssex  15173  ssblex  15174  blin2  15175  bdmetval  15243  xmetxp  15250  xmettx  15253  metcnpi3  15260  txmetcnp  15261  addcncntoplem  15304  fsumcncntop  15310  elcncf2  15317  mulc1cncf  15332  cncfco  15334  cncfmet  15335  cncfmptc  15339  mulcncf  15351  dedekindeulemub  15361  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeu  15366  dedekindicclemub  15370  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemuopn  15381  dich0  15395  limcimo  15408  cnplimccntop  15413  limccnp2lem  15419  limccnp2cntop  15420  dvfvalap  15424  dveflem  15469  plycolemc  15501  plyco  15502  plyrecj  15506  reeff1olem  15514  reeff1oleme  15515  eflt  15518  sin0pilem2  15525  pilem3  15526  ioocosf1o  15597  cxplt  15659  cxple  15660  cxplt3  15663  apcxp2  15682  rprelogbmul  15698  rprelogbdiv  15700  logbgt0b  15709  logbgcd1irrap  15713  mpodvdsmulf1o  15733  fsumdvdsmul  15734  lgsdir2lem5  15780  lgsdi  15785  lgsne0  15786  gausslemma2dlem1f1o  15808  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem2  15830  lgsquad2  15831  2sqlem6  15868  2sqlem8  15871  2sqlem9  15872  2sqlem10  15873  upgredg  16014  usgredg4  16085  uspgredg2vlem  16090  usgr1eop  16115  upgrspanop  16153  umgrspanop  16154  usgrspanop  16155  vtxedgfi  16159  vtxlpfi  16160  iswlkg  16199  upgriswlkdc  16230  upgr2wlkdc  16247  clwwlkccatlem  16270  clwwlknonex2e  16310  nnti  16642  pwtrufal  16649  pwf1oexmid  16651  sssneq  16654  qdencn  16682  cvgcmp2n  16688  trilpolemlt1  16696  trirec0  16699  qdiff  16704  redc0  16713  reap0  16714  cndcap  16715  nconstwlpolemgt0  16720  neap0mkv  16725  supfz  16727  inffz  16728  gfsumval  16732  gfsumcl  16739