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  4681  reg3exmidlemwe  4726  nnsucpred  4764  iotam  5369  fvmptt  5797  fcof1  5989  fliftfun  6002  isotr  6022  riotass2  6067  acexmidlemab  6079  ovmpodf  6220  fnmpoovd  6451  1stconst  6457  2ndconst  6458  cnvf1olem  6460  f1od2  6471  suppcofn  6506  smoiso  6573  tfrcldm  6634  tfrcl  6635  nntr2  6776  swoer  6835  erinxp  6883  ecopovsymg  6908  th3qlem1  6911  f1imaen2g  7080  pw2f1odclem  7134  mapdom1g  7147  fict  7170  fidifsnen  7172  dif1enen  7184  fiunsnnn  7185  fisbth  7187  findcard2d  7195  findcard2sd  7196  diffifi  7198  ac6sfi  7202  fimax2gtri  7206  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  ssfirab  7244  exmidssfi  7246  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlemi6  7279  sbthlemi8  7281  isbth  7284  fiuni  7312  supmaxti  7344  infminti  7367  ordiso2  7375  eldju2ndl  7412  eldju2ndr  7413  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctmlemr  7448  ctssdccl  7451  nninfninc  7463  fodjum  7486  fodju0  7487  omniwomnimkv  7507  exmidfodomrlemrALT  7555  acfun  7563  exmidaclem  7564  netap  7620  exmidmotap  7627  ccfunen  7630  cc1  7631  cc2lem  7632  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  enq0sym  7799  enq0tr  7801  distrnq0  7826  prarloclem3  7864  genplt2i  7877  addlocpr  7903  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprg  7986  prplnqu  7987  addextpr  7988  recexprlemdisj  7997  recexprlemloc  7998  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemaddq  8075  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  recexgt0sr  8140  mulgt0sr  8145  prsrriota  8155  suplocsrlem  8175  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axmulcom  8238  rereceu  8256  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  addcan  8506  addcan2  8507  addsub4  8569  ltadd2  8747  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  eqord1  8811  rereim  8914  apreap  8915  apreim  8931  mulreim  8932  apcotr  8935  apadd1  8936  addext  8938  apneg  8939  mulext1  8940  mulext  8942  ltleap  8960  aprcl  8974  mulap0  8982  mulcanapd  8989  recapb  9001  rec11ap  9040  rec11rap  9041  divdivdivap  9043  ddcanap  9056  divadddivap  9057  prodgt0gt0  9181  prodgt0  9182  prodge0  9184  lemulge11  9196  lt2mul2div  9209  ltrec  9213  lerec  9214  lerec2  9219  ledivp1  9233  mulle0r  9274  nn0ge0div  9733  suprzclex  9744  qapne  10039  xrlelttr  10208  xrltletr  10209  xrre3  10224  xrrege0  10227  xaddge0  10280  xle2add  10281  xlt2add  10282  fzass4  10468  fzrev  10491  elfz1b  10497  eluzgtdifelfzo  10615  fzocatel  10617  zsupcllemstep  10662  zsupcllemex  10663  zssinfcl  10665  infssfzcldc  10669  infssfzledc  10670  suprzubdc  10671  exbtwnzlemex  10684  rebtwn2z  10689  modqid  10786  modqcyc  10796  modqaddabs  10799  modqaddmod  10800  mulqaddmodid  10801  modqadd2mod  10811  modqltm1p1mod  10813  modqsubmod  10819  modqsubmodmod  10820  modaddmodup  10824  modqmulmod  10826  modqmulmodr  10827  modqaddmulmod  10828  modqsubdir  10830  frec2uzisod  10844  uzennn  10873  iseqovex  10895  seqvalcd  10898  seq1g  10900  seqf  10901  seqovcd  10904  seqclg  10909  seqm1g  10911  seq3shft2  10918  seqshft2g  10919  monoord  10922  iseqf1olemnab  10938  seqf1oglem1  10956  seqf1og  10958  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  expnegzap  11010  ltexp2a  11028  le2sq2  11052  bernneq  11098  expnlbnd2  11103  nn0ltexp2  11147  nn0opth2  11162  faclbnd  11179  bcval5  11201  hashcl  11220  hashen  11223  fihashdom  11243  hashunlem  11244  hashun  11245  hashxp  11267  hashmap  11268  fimaxq  11270  sseqn  11279  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  hashf1  11287  zfz1isolem1  11292  zfz1iso  11293  seq3coll  11294  sswrd  11313  ccatw2s1p1g  11413  ccatw2s1p2  11414  ccat2s1fstg  11416  wrdind  11494  pfxccatin12lem1  11500  pfxccatin12lem3  11504  reuccatpfxs1lem  11518  cvg1nlemres  11751  cvg1n  11752  resqrexlemp1rp  11772  resqrexlemoverl  11787  resqrexlemex  11791  sqrtsq  11810  abslt  11854  absle  11855  abs3lem  11877  maxleastlt  11981  maxltsup  11984  fimaxre2  11993  negfi  11994  xrmaxleastlt  12022  xrmaxltsup  12024  xrmaxaddlem  12026  2clim  12067  climcn2  12075  addcn2  12076  mulcn2  12078  reccn2ap  12079  climge0  12091  climcau  12113  fzf1o  12142  summodclem2  12149  summodc  12150  zsumdc  12151  fsumf1o  12157  fisumss  12159  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  mptfzshft  12209  fsumrev  12210  fsummulc2  12215  fsumconst  12221  modfsummod  12225  fsumrelem  12238  binom  12251  cvgratnn  12298  mertenslemub  12301  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodf1o  12355  fprodssdc  12357  fprodmul  12358  fprodcl2lem  12372  fprodrev  12386  fprodconst  12387  fprodap0  12388  fprodrec  12396  fprodap0f  12403  fprodle  12407  fprodmodd  12408  efcllem  12426  tanaddaplem  12505  moddvds  12566  dvdsflip  12618  oexpneg  12644  nn0o  12674  fldivndvdslt  12704  bitsfi  12724  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemeu  12784  dfgcd3  12787  dfgcd2  12791  dvdsmulgcd  12802  bezoutr  12809  nninfctlemfo  12817  lcmgcdlem  12855  coprmdvds2  12871  qredeu  12875  rpdvds  12877  cncongr1  12881  prmind2  12898  isprm5lem  12919  isprm6  12925  oddpwdclemdc  12951  nonsq  12985  hashdvds  12999  crth  13002  eulerthlemh  13009  prmdiveq  13014  hashgcdlem  13016  hashgcdeq  13018  nnnn0modprm0  13034  pclemub  13066  pceu  13074  pcmul  13080  pcqmul  13082  pcgcd1  13107  pc2dvds  13109  difsqpwdvds  13117  pcmpt  13122  prmpwdvds  13134  1arith  13146  mul4sq  13173  4sqlemafi  13174  4sqlemffi  13175  4sqexercise2  13178  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemg  13294  ennnfonelemex  13305  ennnfonelemrnh  13307  ennnfonelemf1  13309  ennnfonelemrn  13310  ennnfonelemdm  13311  ennnfonelemim  13315  ennnfone  13316  ctinf  13321  ctiunctlemfo  13330  nninfdclemcl  13339  nninfdclemf  13340  nninfdclemp1  13341  unbendc  13345  isstruct2r  13363  setscom  13392  ercpbl  13652  opifismgmdc  13691  grpinvalem  13705  gzsumvalx  13709  gzsumfzval  13711  gzsumval2  13714  sgrppropd  13728  mndpropd  13753  issubmnd  13755  submnd0  13757  mhmf1o  13777  subsubm  13790  0mhm  13793  resmhm  13794  mhmco  13797  mhmima  13798  mhmeql  13799  gzsumwsubmcl  13801  gzsumcl  13804  grprcan  13842  grpinvid1  13857  grpinvid2  13858  grplcan  13867  grplmulf1o  13879  grpnpncan0  13901  dfgrp3mlem  13903  grplactcnv  13907  mulgval  13925  mulgfng  13927  mulgnngzsum  13930  mulg1  13932  mulgnnp1  13933  mulgneg  13943  mulgnndir  13954  mulgdirlem  13956  mulgnn0ass  13961  mulgass  13962  subgmulg  13991  issubg4m  13996  subsubg  14000  subgintm  14001  isnsg3  14010  eqgcpbl  14031  ghmeql  14070  ghmnsgima  14071  ghmnsgpreima  14072  ghmf1  14076  ghmf1o  14078  conjghm  14079  qusghm  14085  cmnsubm  14112  ablpncan3  14121  invghm  14133  eqgabl  14134  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gsumvalfi  14152  gsumzfi  14158  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsumconstcmn  14166  prdssgrpd  14191  prdsmndd  14194  pwssub  14216  rngpropd  14254  imasrng  14255  qusrng  14257  srglmhm  14297  srgrmhm  14298  ringpropd  14343  ringlghm  14366  ringrghm  14367  imasring  14369  qusring2  14371  opprrngbg  14383  dvdsrvald  14400  dvdsrd  14401  dvdsrex  14405  dvdsrtr  14408  unitpropdg  14455  rhmopp  14483  isnzr2  14491  issubrng2  14518  subrngintm  14520  subsubrng  14522  subrgintm  14551  subsubrg  14553  rhmpropd  14562  ringunitap  14593  aprap  14598  drngunitap  14608  lmodprop2d  14685  rmodislmod  14688  lssvacl  14702  lssvsubcl  14703  lssvscl  14712  islss3  14716  lss1d  14720  rnglidlmcl  14817  2idlcpblrng  14860  crngridl  14867  gsumfsum  14923  expghmap  14942  mulgghm2  14943  mulgrhm  14944  znf1o  14986  znleval  14988  znidom  14992  znidomb  14993  znunit  14994  asclghm  15025  issubassa2  15035  assamulgscmlem2  15042  psrbagcon  15062  mplsubgfilemcl  15090  iuncld  15216  ssnei2  15258  topssnei  15263  restopnb  15282  cnfval  15295  cnpfval  15296  iscnp4  15319  cnptopco  15323  cncnpi  15329  cncnp  15331  cnconst2  15334  cnrest2  15337  cnptoprest  15340  cnptoprest2  15341  cnpdis  15343  lmss  15347  lmtopcnp  15351  neitx  15369  txcnp  15372  txrest  15377  txdis1cn  15379  txlm  15380  cnmpt21  15392  imasnopn  15400  xmetres2  15480  blvalps  15489  blval  15490  elbl2ps  15493  elbl2  15494  blhalf  15509  blssexps  15530  blssex  15531  ssblex  15532  blin2  15533  bdmetval  15601  xmetxp  15608  xmettx  15611  metcnpi3  15618  txmetcnp  15619  addcncntoplem  15662  fsumcncntop  15668  elcncf2  15675  mulc1cncf  15690  cncfco  15692  cncfmet  15693  cncfmptc  15697  mulcncf  15709  dedekindeulemub  15719  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeu  15724  dedekindicclemub  15728  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemicc  15733  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemuopn  15739  dich0  15753  limcimo  15766  cnplimccntop  15771  limccnp2lem  15777  limccnp2cntop  15778  dvfvalap  15782  dveflem  15827  plycolemc  15859  plyco  15860  plyrecj  15864  reeff1olem  15872  reeff1oleme  15873  eflt  15876  sin0pilem2  15883  pilem3  15884  ioocosf1o  15955  cxplt  16018  cxple  16019  cxplt3  16022  apcxp2  16041  rprelogbmul  16057  rprelogbdiv  16059  logbgt0b  16068  logbgcd1irrap  16072  pellexlem3  16093  mpodvdsmulf1o  16104  fsumdvdsmul  16105  lgsdir2lem5  16151  lgsdi  16156  lgsne0  16157  gausslemma2dlem1f1o  16179  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad2lem2  16201  lgsquad2  16202  2sqlem6  16239  2sqlem8  16242  2sqlem9  16243  2sqlem10  16244  upgredg  16385  usgredg4  16456  uspgredg2vlem  16461  usgr1eop  16486  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  vtxedgfi  16530  vtxlpfi  16531  iswlkg  16570  upgriswlkdc  16601  upgr2wlkdc  16618  clwwlkccatlem  16641  clwwlknonex2e  16681  nnti  17022  pwtrufal  17027  pwf1oexmid  17029  sssneq  17032  qdencn  17072  cvgcmp2n  17082  trilpolemlt1  17090  trirec0  17093  qdiff  17098  redc0  17107  reap0  17108  cndcap  17109  nconstwlpolemgt0  17114  neap0mkv  17119  supfz  17121  inffz  17122