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  5923  fliftfun  5936  isotr  5956  riotass2  5999  acexmidlemab  6011  ovmpodf  6152  fnmpoovd  6379  1stconst  6385  2ndconst  6386  cnvf1olem  6388  f1od2  6399  smoiso  6467  tfrcldm  6528  tfrcl  6529  nntr2  6670  swoer  6729  erinxp  6777  ecopovsymg  6802  th3qlem1  6805  f1imaen2g  6966  pw2f1odclem  7019  mapdom1g  7032  fict  7054  fidifsnen  7056  dif1enen  7068  fiunsnnn  7069  fisbth  7071  findcard2d  7079  findcard2sd  7080  diffifi  7082  ac6sfi  7086  fimax2gtri  7090  nnwetri  7107  unsnfi  7110  unsnfidcex  7111  unsnfidcel  7112  fisseneq  7126  ssfirab  7128  exmidssfi  7130  fidcenumlemrk  7152  fidcenumlemr  7153  sbthlemi6  7160  sbthlemi8  7162  isbth  7165  fiuni  7176  supmaxti  7202  infminti  7225  ordiso2  7233  eldju2ndl  7270  eldju2ndr  7271  omp1eomlem  7292  difinfsnlem  7297  difinfinf  7299  ctmlemr  7306  ctssdccl  7309  nninfninc  7321  fodjum  7344  fodju0  7345  omniwomnimkv  7365  exmidfodomrlemrALT  7413  acfun  7421  exmidaclem  7422  netap  7472  exmidmotap  7479  ccfunen  7482  cc1  7483  cc2lem  7484  dfplpq2  7573  dfmpq2  7574  mulpipqqs  7592  distrnqg  7606  enq0sym  7651  enq0tr  7653  distrnq0  7678  prarloclem3  7716  genplt2i  7729  addlocpr  7755  prmuloc  7785  distrlem1prl  7801  distrlem1pru  7802  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  ltaprg  7838  prplnqu  7839  addextpr  7840  recexprlemdisj  7849  recexprlemloc  7850  aptiprleml  7858  aptiprlemu  7859  ltmprr  7861  archpr  7862  cauappcvgprlemopl  7865  cauappcvgprlemopu  7867  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  caucvgprlemnkj  7885  caucvgprlemopl  7888  caucvgprlemopu  7890  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemopu  7918  caucvgprprlemdisj  7921  caucvgprprlemloc  7922  caucvgprprlemaddq  7927  suplocexprlemrl  7936  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemex  7941  suplocexprlemub  7942  recexgt0sr  7992  mulgt0sr  7997  prsrriota  8007  suplocsrlem  8027  addcnsr  8053  mulcnsr  8054  mulcnsrec  8062  axmulcom  8090  rereceu  8108  axarch  8110  axcaucvglemres  8118  axpre-suploclemres  8120  lelttr  8267  ltletr  8268  addcan  8358  addcan2  8359  addsub4  8421  ltadd2  8598  le2add  8623  lt2add  8624  lt2sub  8639  le2sub  8640  eqord1  8662  rereim  8765  apreap  8766  apreim  8782  mulreim  8783  apcotr  8786  apadd1  8787  addext  8789  apneg  8790  mulext1  8791  mulext  8793  ltleap  8811  aprcl  8825  mulap0  8833  mulcanapd  8840  recapb  8850  rec11ap  8889  rec11rap  8890  divdivdivap  8892  ddcanap  8905  divadddivap  8906  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  lemulge11  9045  lt2mul2div  9058  ltrec  9062  lerec  9063  lerec2  9068  ledivp1  9082  mulle0r  9123  nn0ge0div  9566  suprzclex  9577  qapne  9872  xrlelttr  10040  xrltletr  10041  xrre3  10056  xrrege0  10059  xaddge0  10112  xle2add  10113  xlt2add  10114  fzass4  10296  fzrev  10318  elfz1b  10324  eluzgtdifelfzo  10441  fzocatel  10443  zsupcllemstep  10488  zsupcllemex  10489  zssinfcl  10491  suprzubdc  10495  exbtwnzlemex  10508  rebtwn2z  10513  modqid  10610  modqcyc  10620  modqaddabs  10623  modqaddmod  10624  mulqaddmodid  10625  modqadd2mod  10635  modqltm1p1mod  10637  modqsubmod  10643  modqsubmodmod  10644  modaddmodup  10648  modqmulmod  10650  modqmulmodr  10651  modqaddmulmod  10652  modqsubdir  10654  frec2uzisod  10668  uzennn  10697  iseqovex  10719  seqvalcd  10722  seq1g  10724  seqf  10725  seqovcd  10728  seqclg  10733  seqm1g  10735  seq3shft2  10742  seqshft2g  10743  monoord  10746  iseqf1olemnab  10762  seqf1oglem1  10780  seqf1og  10782  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  expnegzap  10834  ltexp2a  10852  le2sq2  10876  bernneq  10921  expnlbnd2  10926  nn0ltexp2  10970  nn0opth2  10985  faclbnd  11002  bcval5  11024  hashcl  11042  hashen  11045  fihashdom  11065  hashunlem  11066  hashun  11067  hashxp  11089  fimaxq  11090  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  sswrd  11121  ccatw2s1p1g  11221  ccatw2s1p2  11222  ccat2s1fstg  11224  wrdind  11302  pfxccatin12lem1  11308  pfxccatin12lem3  11312  reuccatpfxs1lem  11326  cvg1nlemres  11545  cvg1n  11546  resqrexlemp1rp  11566  resqrexlemoverl  11581  resqrexlemex  11585  sqrtsq  11604  abslt  11648  absle  11649  abs3lem  11671  maxleastlt  11775  maxltsup  11778  fimaxre2  11787  negfi  11788  xrmaxleastlt  11816  xrmaxltsup  11818  xrmaxaddlem  11820  2clim  11861  climcn2  11869  addcn2  11870  mulcn2  11872  reccn2ap  11873  climge0  11885  climcau  11907  summodclem2  11942  summodc  11943  zsumdc  11944  fsumf1o  11950  fisumss  11952  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  mptfzshft  12002  fsumrev  12003  fsummulc2  12008  fsumconst  12014  modfsummod  12018  fsumrelem  12031  binom  12044  cvgratnn  12091  mertenslemub  12094  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodf1o  12148  fprodssdc  12150  fprodmul  12151  fprodcl2lem  12165  fprodrev  12179  fprodconst  12180  fprodap0  12181  fprodrec  12189  fprodap0f  12196  fprodle  12200  fprodmodd  12201  efcllem  12219  tanaddaplem  12298  moddvds  12359  dvdsflip  12411  oexpneg  12437  nn0o  12467  fldivndvdslt  12497  bitsfi  12517  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemeu  12577  dfgcd3  12580  dfgcd2  12584  dvdsmulgcd  12595  bezoutr  12602  nninfctlemfo  12610  lcmgcdlem  12648  coprmdvds2  12664  qredeu  12668  rpdvds  12670  cncongr1  12674  prmind2  12691  isprm5lem  12712  isprm6  12718  oddpwdclemdc  12744  nonsq  12778  hashdvds  12792  crth  12795  eulerthlemh  12802  prmdiveq  12807  hashgcdlem  12809  hashgcdeq  12811  nnnn0modprm0  12827  pclemub  12859  pceu  12867  pcmul  12873  pcqmul  12875  pcgcd1  12900  pc2dvds  12902  difsqpwdvds  12910  pcmpt  12915  prmpwdvds  12927  1arith  12939  mul4sq  12966  4sqlemafi  12967  4sqlemffi  12968  4sqexercise2  12971  ennnfonelemg  13023  ennnfonelemex  13034  ennnfonelemrnh  13036  ennnfonelemf1  13038  ennnfonelemrn  13039  ennnfonelemdm  13040  ennnfonelemim  13044  ennnfone  13045  ctinf  13050  ctiunctlemfo  13059  nninfdclemcl  13068  nninfdclemf  13069  nninfdclemp1  13070  unbendc  13074  isstruct2r  13092  setscom  13121  ercpbl  13413  opifismgmdc  13453  grpinvalem  13467  igsumvalx  13471  gsumfzval  13473  gsumval2  13479  sgrppropd  13495  prdssgrpd  13497  mndpropd  13522  issubmnd  13524  submnd0  13526  prdsmndd  13530  mhmf1o  13552  subsubm  13565  0mhm  13568  resmhm  13569  mhmco  13572  mhmima  13573  mhmeql  13574  gsumfzz  13577  gsumwsubmcl  13578  gsumfzcl  13581  grprcan  13619  grpinvid1  13634  grpinvid2  13635  grplcan  13644  grplmulf1o  13656  grpnpncan0  13678  dfgrp3mlem  13680  grplactcnv  13684  pwssub  13695  mulgval  13708  mulgfng  13710  mulgnngsum  13713  mulg1  13715  mulgnnp1  13716  mulgneg  13726  mulgnndir  13737  mulgdirlem  13739  mulgnn0ass  13744  mulgass  13745  subgmulg  13774  issubg4m  13779  subsubg  13783  subgintm  13784  isnsg3  13793  eqgcpbl  13814  ghmeql  13853  ghmnsgima  13854  ghmnsgpreima  13855  ghmf1  13859  ghmf1o  13861  conjghm  13862  qusghm  13868  ablpncan3  13903  invghm  13915  eqgabl  13916  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  rngpropd  13967  imasrng  13968  qusrng  13970  srglmhm  14005  srgrmhm  14006  ringpropd  14050  ringlghm  14073  ringrghm  14074  imasring  14076  qusring2  14078  opprrngbg  14090  dvdsrvald  14106  dvdsrd  14107  dvdsrex  14111  dvdsrtr  14114  unitpropdg  14161  rhmopp  14189  isnzr2  14197  issubrng2  14223  subrngintm  14225  subsubrng  14227  subrgintm  14256  subsubrg  14258  rhmpropd  14267  aprap  14299  lmodprop2d  14361  rmodislmod  14364  lssvacl  14378  lssvsubcl  14379  lssvscl  14388  islss3  14392  lss1d  14396  rnglidlmcl  14493  2idlcpblrng  14536  crngridl  14543  expghmap  14620  mulgghm2  14621  mulgrhm  14622  znf1o  14664  znleval  14666  znidom  14670  znidomb  14671  znunit  14672  mplsubgfilemcl  14712  iuncld  14838  ssnei2  14880  topssnei  14885  restopnb  14904  cnfval  14917  cnpfval  14918  iscnp4  14941  cnptopco  14945  cncnpi  14951  cncnp  14953  cnconst2  14956  cnrest2  14959  cnptoprest  14962  cnptoprest2  14963  cnpdis  14965  lmss  14969  lmtopcnp  14973  neitx  14991  txcnp  14994  txrest  14999  txdis1cn  15001  txlm  15002  cnmpt21  15014  imasnopn  15022  xmetres2  15102  blvalps  15111  blval  15112  elbl2ps  15115  elbl2  15116  blhalf  15131  blssexps  15152  blssex  15153  ssblex  15154  blin2  15155  bdmetval  15223  xmetxp  15230  xmettx  15233  metcnpi3  15240  txmetcnp  15241  addcncntoplem  15284  fsumcncntop  15290  elcncf2  15297  mulc1cncf  15312  cncfco  15314  cncfmet  15315  cncfmptc  15319  mulcncf  15331  dedekindeulemub  15341  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeu  15346  dedekindicclemub  15350  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemuopn  15361  dich0  15375  limcimo  15388  cnplimccntop  15393  limccnp2lem  15399  limccnp2cntop  15400  dvfvalap  15404  dveflem  15449  plycolemc  15481  plyco  15482  plyrecj  15486  reeff1olem  15494  reeff1oleme  15495  eflt  15498  sin0pilem2  15505  pilem3  15506  ioocosf1o  15577  cxplt  15639  cxple  15640  cxplt3  15643  apcxp2  15662  rprelogbmul  15678  rprelogbdiv  15680  logbgt0b  15689  logbgcd1irrap  15693  mpodvdsmulf1o  15713  fsumdvdsmul  15714  lgsdir2lem5  15760  lgsdi  15765  lgsne0  15766  gausslemma2dlem1f1o  15788  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem2  15810  lgsquad2  15811  2sqlem6  15848  2sqlem8  15851  2sqlem9  15852  2sqlem10  15853  upgredg  15994  usgredg4  16065  uspgredg2vlem  16070  usgr1eop  16095  upgrspanop  16133  umgrspanop  16134  usgrspanop  16135  vtxedgfi  16139  vtxlpfi  16140  iswlkg  16179  upgriswlkdc  16210  upgr2wlkdc  16227  clwwlkccatlem  16250  clwwlknonex2e  16290  nnti  16591  pwtrufal  16598  pwf1oexmid  16600  sssneq  16603  qdencn  16631  cvgcmp2n  16637  trilpolemlt1  16645  trirec0  16648  redc0  16661  reap0  16662  cndcap  16663  nconstwlpolemgt0  16668  neap0mkv  16673  supfz  16675  inffz  16676  gfsumval  16680