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  7345  infminti  7368  ordiso2  7376  eldju2ndl  7413  eldju2ndr  7414  omp1eomlem  7435  difinfsnlem  7440  difinfinf  7442  ctmlemr  7449  ctssdccl  7452  nninfninc  7464  fodjum  7487  fodju0  7488  omniwomnimkv  7508  exmidfodomrlemrALT  7556  acfun  7564  exmidaclem  7565  netap  7621  exmidmotap  7628  ccfunen  7631  cc1  7632  cc2lem  7633  dfplpq2  7722  dfmpq2  7723  mulpipqqs  7741  distrnqg  7755  enq0sym  7800  enq0tr  7802  distrnq0  7827  prarloclem3  7865  genplt2i  7878  addlocpr  7904  prmuloc  7934  distrlem1prl  7950  distrlem1pru  7951  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltaprg  7987  prplnqu  7988  addextpr  7989  recexprlemdisj  7998  recexprlemloc  7999  aptiprleml  8007  aptiprlemu  8008  ltmprr  8010  archpr  8011  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnjltk  8059  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemdisj  8070  caucvgprprlemloc  8071  caucvgprprlemaddq  8076  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  recexgt0sr  8141  mulgt0sr  8146  prsrriota  8156  suplocsrlem  8176  addcnsr  8202  mulcnsr  8203  mulcnsrec  8211  axmulcom  8239  rereceu  8257  axarch  8259  axcaucvglemres  8267  axpre-suploclemres  8269  lelttr  8415  ltletr  8416  addcan  8508  addcan2  8509  addsub4  8571  ltadd2  8749  le2add  8774  lt2add  8775  lt2sub  8790  le2sub  8791  eqord1  8813  rereim  8917  apreap  8918  apreim  8934  mulreim  8935  apcotr  8938  apadd1  8939  addext  8941  apneg  8942  mulext1  8943  mulext  8945  ltleap  8963  aprcl  8977  mulap0  8985  mulcanapd  8992  recapb  9004  rec11ap  9043  rec11rap  9044  divdivdivap  9046  ddcanap  9059  divadddivap  9060  prodgt0gt0  9184  prodgt0  9185  prodge0  9187  lemulge11  9199  lt2mul2div  9212  ltrec  9216  lerec  9217  lerec2  9222  ledivp1  9236  mulle0r  9277  nn0ge0div  9738  suprzclex  9749  qapne  10049  xrlelttr  10219  xrltletr  10220  xrre3  10235  xrrege0  10238  xaddge0  10291  xle2add  10292  xlt2add  10293  fzass4  10479  fzrev  10502  elfz1b  10508  eluzgtdifelfzo  10626  fzocatel  10628  zsupcllemstep  10673  zsupcllemex  10674  zssinfcl  10676  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  exbtwnzlemex  10695  rebtwn2z  10700  modqid  10801  modqcyc  10811  modqaddabs  10814  modqaddmod  10815  mulqaddmodid  10816  modqadd2mod  10826  modqltm1p1mod  10828  modqsubmod  10834  modqsubmodmod  10835  modaddmodup  10839  modqmulmod  10841  modqmulmodr  10842  modqaddmulmod  10843  modqsubdir  10845  frec2uzisod  10859  uzennn  10888  iseqovex  10910  seqvalcd  10913  seq1g  10915  seqf  10916  seqovcd  10919  seqclg  10924  seqm1g  10926  seq3shft2  10933  seqshft2g  10934  monoord  10937  iseqf1olemnab  10953  seqf1oglem1  10971  seqf1og  10973  seqhomog  10982  seqfeq4g  10983  seq3distr  10984  expnegzap  11025  ltexp2a  11043  le2sq2  11067  bernneq  11113  expnlbnd2  11118  nn0ltexp2  11163  nn0opth2  11178  faclbnd  11195  bcval5  11217  hashcl  11236  hashen  11239  fihashdom  11259  hashunlem  11260  hashun  11261  hashxp  11283  hashmap  11284  fimaxq  11286  sseqn  11295  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  hashf1  11303  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  sswrd  11329  ccatw2s1p1g  11429  ccatw2s1p2  11430  ccat2s1fstg  11432  wrdind  11510  pfxccatin12lem1  11516  pfxccatin12lem3  11520  reuccatpfxs1lem  11534  cvg1nlemres  11767  cvg1n  11768  resqrexlemp1rp  11788  resqrexlemoverl  11803  resqrexlemex  11807  sqrtsq  11826  abslt  11871  absle  11872  abs3lem  11894  maxleastlt  11998  maxltsup  12001  fimaxre2  12010  negfi  12011  fiidxsupcl  12012  xrmaxleastlt  12041  xrmaxltsup  12043  xrmaxaddlem  12045  2clim  12086  climcn2  12094  addcn2  12095  mulcn2  12097  reccn2ap  12098  climge0  12110  climcau  12132  fzf1o  12161  summodclem2  12168  summodc  12169  zsumdc  12170  fsumf1o  12176  fisumss  12178  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  mptfzshft  12228  fsumrev  12229  fsummulc2  12234  fsumconst  12240  modfsummod  12244  fsumrelem  12257  binom  12270  cvgratnn  12317  mertenslemub  12320  prodmodclem2  12363  prodmodc  12364  zproddc  12365  fprodf1o  12374  fprodssdc  12376  fprodmul  12377  fprodcl2lem  12391  fprodrev  12405  fprodconst  12406  fprodap0  12407  fprodrec  12415  fprodap0f  12422  fprodle  12426  fprodmodd  12427  efcllem  12445  tanaddaplem  12524  moddvds  12585  dvdsflip  12637  oexpneg  12663  nn0o  12693  fldivndvdslt  12723  bitsfi  12743  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemeu  12803  dfgcd3  12806  dfgcd2  12810  dvdsmulgcd  12821  bezoutr  12828  nninfctlemfo  12836  lcmgcdlem  12874  coprmdvds2  12890  qredeu  12894  rpdvds  12896  cncongr1  12900  prmind2  12917  isprm5lem  12939  isprm6  12945  nnmaxpwlemparts  12971  nnmaxpw  12972  nonsq  13006  nn0sqdcq  13007  sqrtrirr  13008  hashdvds  13022  crth  13025  eulerthlemh  13032  prmdiveq  13037  hashgcdlem  13039  hashgcdeq  13041  nnnn0modprm0  13057  pclemub  13089  pceu  13097  pcmul  13103  pcqmul  13105  pcgcd1  13130  pc2dvds  13132  difsqpwdvds  13140  pcmpt  13145  prmpwdvds  13157  1arith  13169  mul4sq  13196  4sqlemafi  13197  4sqlemffi  13198  4sqexercise2  13201  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemg  13346  ennnfonelemex  13357  ennnfonelemrnh  13359  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemdm  13363  ennnfonelemim  13367  ennnfone  13368  ctinf  13373  ctiunctlemfo  13382  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  unbendc  13397  isstruct2r  13415  setscom  13444  ercpbl  13705  opifismgmdc  13744  grpinvalem  13758  gzsumvalx  13762  gzsumfzval  13764  gzsumval2  13767  sgrppropd  13781  mndpropd  13806  issubmnd  13808  submnd0  13810  mhmf1o  13830  subsubm  13843  0mhm  13846  resmhm  13847  mhmco  13850  mhmima  13851  mhmeql  13852  gzsumwsubmcl  13854  gzsumcl  13857  grprcan  13895  grpinvid1  13910  grpinvid2  13911  grplcan  13920  grplmulf1o  13932  grpnpncan0  13954  dfgrp3mlem  13956  grplactcnv  13960  mulgval  13978  mulgfng  13980  mulgnngzsum  13983  mulg1  13985  mulgnnp1  13986  mulgneg  13996  mulgnndir  14007  mulgdirlem  14009  mulgnn0ass  14014  mulgass  14015  subgmulg  14044  issubg4m  14049  subsubg  14053  subgintm  14054  isnsg3  14063  eqgcpbl  14084  ghmeql  14123  ghmnsgima  14124  ghmnsgpreima  14125  ghmf1  14129  ghmf1o  14131  conjghm  14132  qusghm  14138  cntzsgrpcl  14161  cntzsubm  14164  cntrsubgnsg  14169  cmnsubm  14196  ablpncan3  14205  invghm  14217  eqgabl  14218  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gsumvalfi  14236  gsumzfi  14242  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsumconstcmn  14250  prdssgrpd  14275  prdsmndd  14278  pwssub  14300  rngpropd  14338  imasrng  14339  qusrng  14341  srglmhm  14381  srgrmhm  14382  ringpropd  14427  ringlghm  14450  ringrghm  14451  imasring  14453  qusring2  14455  opprrngbg  14467  dvdsrvald  14484  dvdsrd  14485  dvdsrex  14489  dvdsrtr  14492  unitpropdg  14539  rhmopp  14567  isnzr2  14575  issubrng2  14602  subrngintm  14604  subsubrng  14606  subrgintm  14635  subsubrg  14637  rhmpropd  14646  ringunitap  14677  aprap  14682  drngunitap  14692  lmodprop2d  14769  rmodislmod  14772  lssvacl  14786  lssvsubcl  14787  lssvscl  14796  islss3  14800  lss1d  14804  rnglidlmcl  14901  2idlcpblrng  14944  crngridl  14951  gsumfsum  15007  expghmap  15026  mulgghm2  15027  mulgrhm  15028  znf1o  15070  znleval  15072  znidom  15076  znidomb  15077  znunit  15078  asclghm  15109  issubassa2  15119  assamulgscmlem2  15126  psrbagcon  15146  psrbaglefifi  15147  mplsubgfilemcl  15181  iuncld  15307  ssnei2  15349  topssnei  15354  restopnb  15373  cnfval  15386  cnpfval  15387  iscnp4  15410  cnptopco  15414  cncnpi  15420  cncnp  15422  cnconst2  15425  cnrest2  15428  cnptoprest  15431  cnptoprest2  15432  cnpdis  15434  lmss  15438  lmtopcnp  15442  neitx  15460  txcnp  15463  txrest  15468  txdis1cn  15470  txlm  15471  cnmpt21  15483  imasnopn  15491  xmetres2  15571  blvalps  15580  blval  15581  elbl2ps  15584  elbl2  15585  blhalf  15600  blssexps  15621  blssex  15622  ssblex  15623  blin2  15624  bdmetval  15692  xmetxp  15699  xmettx  15702  metcnpi3  15709  txmetcnp  15710  addcncntoplem  15753  fsumcncntop  15759  elcncf2  15766  mulc1cncf  15781  cncfco  15783  cncfmet  15784  cncfmptc  15788  mulcncf  15800  dedekindeulemub  15810  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeu  15815  dedekindicclemub  15819  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicclemicc  15824  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemuopn  15830  dich0  15844  limcimo  15857  cnplimccntop  15862  limccnp2lem  15868  limccnp2cntop  15869  dvfvalap  15873  dveflem  15918  plycolemc  15950  plyco  15951  plyrecj  15955  reeff1olem  15963  reeff1oleme  15964  eflt  15967  sin0pilem2  15975  pilem3  15976  ioocosf1o  16047  logdivlt  16088  logdivle  16089  cxplt  16113  cxple  16114  cxplt3  16117  apcxp2  16136  rprelogbmul  16152  rprelogbdiv  16154  logbgt0b  16163  logbgcd1irrap  16167  zprmlogbap  16179  pellexlem3  16192  ppinprm  16221  chtnprm  16223  mpodvdsmulf1o  16245  fsumdvdsmul  16246  chtublem  16256  bposlem3  16274  lgsdir2lem5  16317  lgsdi  16322  lgsne0  16323  gausslemma2dlem1f1o  16345  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad2lem2  16367  lgsquad2  16368  2sqlem6  16405  2sqlem8  16408  2sqlem9  16409  2sqlem10  16410  upgredg  16551  usgredg4  16622  uspgredg2vlem  16627  usgr1eop  16652  upgrspanop  16690  umgrspanop  16691  usgrspanop  16692  vtxedgfi  16696  vtxlpfi  16697  iswlkg  16736  upgriswlkdc  16767  upgr2wlkdc  16784  clwwlkccatlem  16807  clwwlknonex2e  16847  nnti  17188  pwtrufal  17193  pwf1oexmid  17195  sssneq  17198  qdencn  17238  cvgcmp2n  17248  trilpolemlt1  17257  trirec0  17260  qdiff  17265  redc0  17274  reap0  17275  cndcap  17276  nconstwlpolemgt0  17281  neap0mkv  17286  supfz  17288  inffz  17289