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 )

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  994  simp1rr  1094  simp2rr  1098  simp3rr  1102  elpr2elpr  3896  invdisjrab  4119  disjiun  4120  reg2exmidlema  4676  reg3exmidlemwe  4721  nnsucpred  4759  iotam  5364  fvmptt  5791  fcof1  5979  fliftfun  5992  isotr  6012  riotass2  6057  acexmidlemab  6069  ovmpodf  6210  fnmpoovd  6441  1stconst  6447  2ndconst  6448  cnvf1olem  6450  f1od2  6461  suppcofn  6496  smoiso  6563  tfrcldm  6624  tfrcl  6625  nntr2  6766  swoer  6825  erinxp  6873  ecopovsymg  6898  th3qlem1  6901  f1imaen2g  7070  pw2f1odclem  7124  mapdom1g  7137  fict  7160  fidifsnen  7162  dif1enen  7174  fiunsnnn  7175  fisbth  7177  findcard2d  7185  findcard2sd  7186  diffifi  7188  ac6sfi  7192  fimax2gtri  7196  nnwetri  7213  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  fisseneq  7232  ssfirab  7234  exmidssfi  7236  fidcenumlemrk  7261  fidcenumlemr  7262  sbthlemi6  7269  sbthlemi8  7271  isbth  7274  fiuni  7302  supmaxti  7334  infminti  7357  ordiso2  7365  eldju2ndl  7402  eldju2ndr  7403  omp1eomlem  7424  difinfsnlem  7429  difinfinf  7431  ctmlemr  7438  ctssdccl  7441  nninfninc  7453  fodjum  7476  fodju0  7477  omniwomnimkv  7497  exmidfodomrlemrALT  7545  acfun  7553  exmidaclem  7554  netap  7610  exmidmotap  7617  ccfunen  7620  cc1  7621  cc2lem  7622  dfplpq2  7711  dfmpq2  7712  mulpipqqs  7730  distrnqg  7744  enq0sym  7789  enq0tr  7791  distrnq0  7816  prarloclem3  7854  genplt2i  7867  addlocpr  7893  prmuloc  7923  distrlem1prl  7939  distrlem1pru  7940  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemfl  7966  ltexprlemrl  7967  ltexprlemfu  7968  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  ltaprg  7976  prplnqu  7977  addextpr  7978  recexprlemdisj  7987  recexprlemloc  7988  aptiprleml  7996  aptiprlemu  7997  ltmprr  7999  archpr  8000  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlem1  8016  cauappcvgprlemlim  8018  caucvgprlemnkj  8023  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnjltk  8048  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemdisj  8059  caucvgprprlemloc  8060  caucvgprprlemaddq  8065  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  recexgt0sr  8130  mulgt0sr  8135  prsrriota  8145  suplocsrlem  8165  addcnsr  8191  mulcnsr  8192  mulcnsrec  8200  axmulcom  8228  rereceu  8246  axarch  8248  axcaucvglemres  8256  axpre-suploclemres  8258  lelttr  8404  ltletr  8405  addcan  8496  addcan2  8497  addsub4  8559  ltadd2  8737  le2add  8762  lt2add  8763  lt2sub  8778  le2sub  8779  eqord1  8801  rereim  8904  apreap  8905  apreim  8921  mulreim  8922  apcotr  8925  apadd1  8926  addext  8928  apneg  8929  mulext1  8930  mulext  8932  ltleap  8950  aprcl  8964  mulap0  8972  mulcanapd  8979  recapb  8991  rec11ap  9030  rec11rap  9031  divdivdivap  9033  ddcanap  9046  divadddivap  9047  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  lemulge11  9186  lt2mul2div  9199  ltrec  9203  lerec  9204  lerec2  9209  ledivp1  9223  mulle0r  9264  nn0ge0div  9712  suprzclex  9723  qapne  10018  xrlelttr  10187  xrltletr  10188  xrre3  10203  xrrege0  10206  xaddge0  10259  xle2add  10260  xlt2add  10261  fzass4  10446  fzrev  10469  elfz1b  10475  eluzgtdifelfzo  10593  fzocatel  10595  zsupcllemstep  10640  zsupcllemex  10641  zssinfcl  10643  infssfzcldc  10647  infssfzledc  10648  suprzubdc  10649  exbtwnzlemex  10662  rebtwn2z  10667  modqid  10764  modqcyc  10774  modqaddabs  10777  modqaddmod  10778  mulqaddmodid  10779  modqadd2mod  10789  modqltm1p1mod  10791  modqsubmod  10797  modqsubmodmod  10798  modaddmodup  10802  modqmulmod  10804  modqmulmodr  10805  modqaddmulmod  10806  modqsubdir  10808  frec2uzisod  10822  uzennn  10851  iseqovex  10873  seqvalcd  10876  seq1g  10878  seqf  10879  seqovcd  10882  seqclg  10887  seqm1g  10889  seq3shft2  10896  seqshft2g  10897  monoord  10900  iseqf1olemnab  10916  seqf1oglem1  10934  seqf1og  10936  seqhomog  10945  seqfeq4g  10946  seq3distr  10947  expnegzap  10988  ltexp2a  11006  le2sq2  11030  bernneq  11076  expnlbnd2  11081  nn0ltexp2  11125  nn0opth2  11140  faclbnd  11157  bcval5  11179  hashcl  11198  hashen  11201  fihashdom  11221  hashunlem  11222  hashun  11223  hashxp  11245  hashmap  11246  fimaxq  11248  sseqn  11257  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  hashf1  11265  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  sswrd  11291  ccatw2s1p1g  11391  ccatw2s1p2  11392  ccat2s1fstg  11394  wrdind  11472  pfxccatin12lem1  11478  pfxccatin12lem3  11482  reuccatpfxs1lem  11496  cvg1nlemres  11729  cvg1n  11730  resqrexlemp1rp  11750  resqrexlemoverl  11765  resqrexlemex  11769  sqrtsq  11788  abslt  11832  absle  11833  abs3lem  11855  maxleastlt  11959  maxltsup  11962  fimaxre2  11971  negfi  11972  xrmaxleastlt  12000  xrmaxltsup  12002  xrmaxaddlem  12004  2clim  12045  climcn2  12053  addcn2  12054  mulcn2  12056  reccn2ap  12057  climge0  12069  climcau  12091  fzf1o  12120  summodclem2  12127  summodc  12128  zsumdc  12129  fsumf1o  12135  fisumss  12137  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  mptfzshft  12187  fsumrev  12188  fsummulc2  12193  fsumconst  12199  modfsummod  12203  fsumrelem  12216  binom  12229  cvgratnn  12276  mertenslemub  12279  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  fprodcl2lem  12350  fprodrev  12364  fprodconst  12365  fprodap0  12366  fprodrec  12374  fprodap0f  12381  fprodle  12385  fprodmodd  12386  efcllem  12404  tanaddaplem  12483  moddvds  12544  dvdsflip  12596  oexpneg  12622  nn0o  12652  fldivndvdslt  12682  bitsfi  12702  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemeu  12762  dfgcd3  12765  dfgcd2  12769  dvdsmulgcd  12780  bezoutr  12787  nninfctlemfo  12795  lcmgcdlem  12833  coprmdvds2  12849  qredeu  12853  rpdvds  12855  cncongr1  12859  prmind2  12876  isprm5lem  12897  isprm6  12903  oddpwdclemdc  12929  nonsq  12963  hashdvds  12977  crth  12980  eulerthlemh  12987  prmdiveq  12992  hashgcdlem  12994  hashgcdeq  12996  nnnn0modprm0  13012  pclemub  13044  pceu  13052  pcmul  13058  pcqmul  13060  pcgcd1  13085  pc2dvds  13087  difsqpwdvds  13095  pcmpt  13100  prmpwdvds  13112  1arith  13124  mul4sq  13151  4sqlemafi  13152  4sqlemffi  13153  4sqexercise2  13156  ballotfilemfc0  13210  ballotfilemfcc  13211  ennnfonelemg  13272  ennnfonelemex  13283  ennnfonelemrnh  13285  ennnfonelemf1  13287  ennnfonelemrn  13288  ennnfonelemdm  13289  ennnfonelemim  13293  ennnfone  13294  ctinf  13299  ctiunctlemfo  13308  nninfdclemcl  13317  nninfdclemf  13318  nninfdclemp1  13319  unbendc  13323  isstruct2r  13341  setscom  13370  ercpbl  13629  opifismgmdc  13668  grpinvalem  13682  gzsumvalx  13686  gzsumfzval  13688  gzsumval2  13691  sgrppropd  13705  mndpropd  13730  issubmnd  13732  submnd0  13734  mhmf1o  13754  subsubm  13767  0mhm  13770  resmhm  13771  mhmco  13774  mhmima  13775  mhmeql  13776  gzsumwsubmcl  13778  gzsumcl  13781  grprcan  13819  grpinvid1  13834  grpinvid2  13835  grplcan  13844  grplmulf1o  13856  grpnpncan0  13878  dfgrp3mlem  13880  grplactcnv  13884  mulgval  13902  mulgfng  13904  mulgnngzsum  13907  mulg1  13909  mulgnnp1  13910  mulgneg  13920  mulgnndir  13931  mulgdirlem  13933  mulgnn0ass  13938  mulgass  13939  subgmulg  13968  issubg4m  13973  subsubg  13977  subgintm  13978  isnsg3  13987  eqgcpbl  14008  ghmeql  14047  ghmnsgima  14048  ghmnsgpreima  14049  ghmf1  14053  ghmf1o  14055  conjghm  14056  qusghm  14062  cmnsubm  14089  ablpncan3  14098  invghm  14110  eqgabl  14111  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gsumvalfi  14129  gsumzfi  14135  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  gsumconstcmn  14143  prdssgrpd  14168  prdsmndd  14171  pwssub  14193  rngpropd  14229  imasrng  14230  qusrng  14232  srglmhm  14271  srgrmhm  14272  ringpropd  14316  ringlghm  14339  ringrghm  14340  imasring  14342  qusring2  14344  opprrngbg  14356  dvdsrvald  14373  dvdsrd  14374  dvdsrex  14378  dvdsrtr  14381  unitpropdg  14428  rhmopp  14456  isnzr2  14464  issubrng2  14491  subrngintm  14493  subsubrng  14495  subrgintm  14524  subsubrg  14526  rhmpropd  14535  ringunitap  14566  aprap  14571  drngunitap  14581  lmodprop2d  14657  rmodislmod  14660  lssvacl  14674  lssvsubcl  14675  lssvscl  14684  islss3  14688  lss1d  14692  rnglidlmcl  14789  2idlcpblrng  14832  crngridl  14839  gsumfsum  14895  expghmap  14914  mulgghm2  14915  mulgrhm  14916  znf1o  14958  znleval  14960  znidom  14964  znidomb  14965  znunit  14966  psrbagcon  14985  mplsubgfilemcl  15013  iuncld  15139  ssnei2  15181  topssnei  15186  restopnb  15205  cnfval  15218  cnpfval  15219  iscnp4  15242  cnptopco  15246  cncnpi  15252  cncnp  15254  cnconst2  15257  cnrest2  15260  cnptoprest  15263  cnptoprest2  15264  cnpdis  15266  lmss  15270  lmtopcnp  15274  neitx  15292  txcnp  15295  txrest  15300  txdis1cn  15302  txlm  15303  cnmpt21  15315  imasnopn  15323  xmetres2  15403  blvalps  15412  blval  15413  elbl2ps  15416  elbl2  15417  blhalf  15432  blssexps  15453  blssex  15454  ssblex  15455  blin2  15456  bdmetval  15524  xmetxp  15531  xmettx  15534  metcnpi3  15541  txmetcnp  15542  addcncntoplem  15585  fsumcncntop  15591  elcncf2  15598  mulc1cncf  15613  cncfco  15615  cncfmet  15616  cncfmptc  15620  mulcncf  15632  dedekindeulemub  15642  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeu  15647  dedekindicclemub  15651  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicclemicc  15656  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemuopn  15662  dich0  15676  limcimo  15689  cnplimccntop  15694  limccnp2lem  15700  limccnp2cntop  15701  dvfvalap  15705  dveflem  15750  plycolemc  15782  plyco  15783  plyrecj  15787  reeff1olem  15795  reeff1oleme  15796  eflt  15799  sin0pilem2  15806  pilem3  15807  ioocosf1o  15878  cxplt  15941  cxple  15942  cxplt3  15945  apcxp2  15964  rprelogbmul  15980  rprelogbdiv  15982  logbgt0b  15991  logbgcd1irrap  15995  pellexlem3  16007  mpodvdsmulf1o  16018  fsumdvdsmul  16019  lgsdir2lem5  16065  lgsdi  16070  lgsne0  16071  gausslemma2dlem1f1o  16093  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem2  16115  lgsquad2  16116  2sqlem6  16153  2sqlem8  16156  2sqlem9  16157  2sqlem10  16158  upgredg  16299  usgredg4  16370  uspgredg2vlem  16375  usgr1eop  16400  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  vtxedgfi  16444  vtxlpfi  16445  iswlkg  16484  upgriswlkdc  16515  upgr2wlkdc  16532  clwwlkccatlem  16555  clwwlknonex2e  16595  nnti  16936  pwtrufal  16941  pwf1oexmid  16943  sssneq  16946  qdencn  16977  cvgcmp2n  16987  trilpolemlt1  16995  trirec0  16998  qdiff  17003  redc0  17012  reap0  17013  cndcap  17014  nconstwlpolemgt0  17019  neap0mkv  17024  supfz  17026  inffz  17027