Theorem simprr 531

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  987  simp1rr  1087  simp2rr  1091  simp3rr  1095  elpr2elpr  3857  invdisjrab  4080  disjiun  4081  reg2exmidlema  4630  reg3exmidlemwe  4675  nnsucpred  4713  iotam  5316  fvmptt  5734  fcof1  5919  fliftfun  5932  isotr  5952  riotass2  5995  acexmidlemab  6007  ovmpodf  6148  fnmpoovd  6375  1stconst  6381  2ndconst  6382  cnvf1olem  6384  f1od2  6395  smoiso  6463  tfrcldm  6524  tfrcl  6525  nntr2  6666  swoer  6725  erinxp  6773  ecopovsymg  6798  th3qlem1  6801  f1imaen2g  6962  pw2f1odclem  7015  mapdom1g  7028  fict  7050  fidifsnen  7052  dif1enen  7062  fiunsnnn  7063  fisbth  7065  findcard2d  7073  findcard2sd  7074  diffifi  7076  ac6sfi  7080  fimax2gtri  7084  nnwetri  7101  unsnfi  7104  unsnfidcex  7105  unsnfidcel  7106  fisseneq  7119  ssfirab  7121  fidcenumlemrk  7144  fidcenumlemr  7145  sbthlemi6  7152  sbthlemi8  7154  isbth  7157  fiuni  7168  supmaxti  7194  infminti  7217  ordiso2  7225  eldju2ndl  7262  eldju2ndr  7263  omp1eomlem  7284  difinfsnlem  7289  difinfinf  7291  ctmlemr  7298  ctssdccl  7301  nninfninc  7313  fodjum  7336  fodju0  7337  omniwomnimkv  7357  exmidfodomrlemrALT  7404  acfun  7412  exmidaclem  7413  netap  7463  exmidmotap  7470  ccfunen  7473  cc1  7474  cc2lem  7475  dfplpq2  7564  dfmpq2  7565  mulpipqqs  7583  distrnqg  7597  enq0sym  7642  enq0tr  7644  distrnq0  7669  prarloclem3  7707  genplt2i  7720  addlocpr  7746  prmuloc  7776  distrlem1prl  7792  distrlem1pru  7793  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemfl  7819  ltexprlemrl  7820  ltexprlemfu  7821  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  ltaprg  7829  prplnqu  7830  addextpr  7831  recexprlemdisj  7840  recexprlemloc  7841  aptiprleml  7849  aptiprlemu  7850  ltmprr  7852  archpr  7853  cauappcvgprlemopl  7856  cauappcvgprlemopu  7858  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  caucvgprlemnkj  7876  caucvgprlemopl  7879  caucvgprlemopu  7881  caucvgprlemdisj  7884  caucvgprlemloc  7885  caucvgprprlemnkltj  7899  caucvgprprlemnkeqj  7900  caucvgprprlemnjltk  7901  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemopu  7909  caucvgprprlemdisj  7912  caucvgprprlemloc  7913  caucvgprprlemaddq  7918  suplocexprlemrl  7927  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemex  7932  suplocexprlemub  7933  recexgt0sr  7983  mulgt0sr  7988  prsrriota  7998  suplocsrlem  8018  addcnsr  8044  mulcnsr  8045  mulcnsrec  8053  axmulcom  8081  rereceu  8099  axarch  8101  axcaucvglemres  8109  axpre-suploclemres  8111  lelttr  8258  ltletr  8259  addcan  8349  addcan2  8350  addsub4  8412  ltadd2  8589  le2add  8614  lt2add  8615  lt2sub  8630  le2sub  8631  eqord1  8653  rereim  8756  apreap  8757  apreim  8773  mulreim  8774  apcotr  8777  apadd1  8778  addext  8780  apneg  8781  mulext1  8782  mulext  8784  ltleap  8802  aprcl  8816  mulap0  8824  mulcanapd  8831  recapb  8841  rec11ap  8880  rec11rap  8881  divdivdivap  8883  ddcanap  8896  divadddivap  8897  prodgt0gt0  9021  prodgt0  9022  prodge0  9024  lemulge11  9036  lt2mul2div  9049  ltrec  9053  lerec  9054  lerec2  9059  ledivp1  9073  mulle0r  9114  nn0ge0div  9557  suprzclex  9568  qapne  9863  xrlelttr  10031  xrltletr  10032  xrre3  10047  xrrege0  10050  xaddge0  10103  xle2add  10104  xlt2add  10105  fzass4  10287  fzrev  10309  elfz1b  10315  eluzgtdifelfzo  10432  fzocatel  10434  zsupcllemstep  10479  zsupcllemex  10480  zssinfcl  10482  suprzubdc  10486  exbtwnzlemex  10499  rebtwn2z  10504  modqid  10601  modqcyc  10611  modqaddabs  10614  modqaddmod  10615  mulqaddmodid  10616  modqadd2mod  10626  modqltm1p1mod  10628  modqsubmod  10634  modqsubmodmod  10635  modaddmodup  10639  modqmulmod  10641  modqmulmodr  10642  modqaddmulmod  10643  modqsubdir  10645  frec2uzisod  10659  uzennn  10688  iseqovex  10710  seqvalcd  10713  seq1g  10715  seqf  10716  seqovcd  10719  seqclg  10724  seqm1g  10726  seq3shft2  10733  seqshft2g  10734  monoord  10737  iseqf1olemnab  10753  seqf1oglem1  10771  seqf1og  10773  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  expnegzap  10825  ltexp2a  10843  le2sq2  10867  bernneq  10912  expnlbnd2  10917  nn0ltexp2  10961  nn0opth2  10976  faclbnd  10993  bcval5  11015  hashcl  11033  hashen  11036  fihashdom  11056  hashunlem  11057  hashun  11058  hashxp  11080  fimaxq  11081  zfz1isolem1  11094  zfz1iso  11095  seq3coll  11096  sswrd  11112  ccatw2s1p1g  11212  ccatw2s1p2  11213  ccat2s1fstg  11215  wrdind  11293  pfxccatin12lem1  11299  pfxccatin12lem3  11303  reuccatpfxs1lem  11317  cvg1nlemres  11536  cvg1n  11537  resqrexlemp1rp  11557  resqrexlemoverl  11572  resqrexlemex  11576  sqrtsq  11595  abslt  11639  absle  11640  abs3lem  11662  maxleastlt  11766  maxltsup  11769  fimaxre2  11778  negfi  11779  xrmaxleastlt  11807  xrmaxltsup  11809  xrmaxaddlem  11811  2clim  11852  climcn2  11860  addcn2  11861  mulcn2  11863  reccn2ap  11864  climge0  11876  climcau  11898  summodclem2  11933  summodc  11934  zsumdc  11935  fsumf1o  11941  fisumss  11943  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  mptfzshft  11993  fsumrev  11994  fsummulc2  11999  fsumconst  12005  modfsummod  12009  fsumrelem  12022  binom  12035  cvgratnn  12082  mertenslemub  12085  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodf1o  12139  fprodssdc  12141  fprodmul  12142  fprodcl2lem  12156  fprodrev  12170  fprodconst  12171  fprodap0  12172  fprodrec  12180  fprodap0f  12187  fprodle  12191  fprodmodd  12192  efcllem  12210  tanaddaplem  12289  moddvds  12350  dvdsflip  12402  oexpneg  12428  nn0o  12458  fldivndvdslt  12488  bitsfi  12508  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemeu  12568  dfgcd3  12571  dfgcd2  12575  dvdsmulgcd  12586  bezoutr  12593  nninfctlemfo  12601  lcmgcdlem  12639  coprmdvds2  12655  qredeu  12659  rpdvds  12661  cncongr1  12665  prmind2  12682  isprm5lem  12703  isprm6  12709  oddpwdclemdc  12735  nonsq  12769  hashdvds  12783  crth  12786  eulerthlemh  12793  prmdiveq  12798  hashgcdlem  12800  hashgcdeq  12802  nnnn0modprm0  12818  pclemub  12850  pceu  12858  pcmul  12864  pcqmul  12866  pcgcd1  12891  pc2dvds  12893  difsqpwdvds  12901  pcmpt  12906  prmpwdvds  12918  1arith  12930  mul4sq  12957  4sqlemafi  12958  4sqlemffi  12959  4sqexercise2  12962  ennnfonelemg  13014  ennnfonelemex  13025  ennnfonelemrnh  13027  ennnfonelemf1  13029  ennnfonelemrn  13030  ennnfonelemdm  13031  ennnfonelemim  13035  ennnfone  13036  ctinf  13041  ctiunctlemfo  13050  nninfdclemcl  13059  nninfdclemf  13060  nninfdclemp1  13061  unbendc  13065  isstruct2r  13083  setscom  13112  ercpbl  13404  opifismgmdc  13444  grpinvalem  13458  igsumvalx  13462  gsumfzval  13464  gsumval2  13470  sgrppropd  13486  prdssgrpd  13488  mndpropd  13513  issubmnd  13515  submnd0  13517  prdsmndd  13521  mhmf1o  13543  subsubm  13556  0mhm  13559  resmhm  13560  mhmco  13563  mhmima  13564  mhmeql  13565  gsumfzz  13568  gsumwsubmcl  13569  gsumfzcl  13572  grprcan  13610  grpinvid1  13625  grpinvid2  13626  grplcan  13635  grplmulf1o  13647  grpnpncan0  13669  dfgrp3mlem  13671  grplactcnv  13675  pwssub  13686  mulgval  13699  mulgfng  13701  mulgnngsum  13704  mulg1  13706  mulgnnp1  13707  mulgneg  13717  mulgnndir  13728  mulgdirlem  13730  mulgnn0ass  13735  mulgass  13736  subgmulg  13765  issubg4m  13770  subsubg  13774  subgintm  13775  isnsg3  13784  eqgcpbl  13805  ghmeql  13844  ghmnsgima  13845  ghmnsgpreima  13846  ghmf1  13850  ghmf1o  13852  conjghm  13853  qusghm  13859  ablpncan3  13894  invghm  13906  eqgabl  13907  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  rngpropd  13958  imasrng  13959  qusrng  13961  srglmhm  13996  srgrmhm  13997  ringpropd  14041  ringlghm  14064  ringrghm  14065  imasring  14067  qusring2  14069  opprrngbg  14081  dvdsrvald  14097  dvdsrd  14098  dvdsrex  14102  dvdsrtr  14105  unitpropdg  14152  rhmopp  14180  isnzr2  14188  issubrng2  14214  subrngintm  14216  subsubrng  14218  subrgintm  14247  subsubrg  14249  rhmpropd  14258  aprap  14290  lmodprop2d  14352  rmodislmod  14355  lssvacl  14369  lssvsubcl  14370  lssvscl  14379  islss3  14383  lss1d  14387  rnglidlmcl  14484  2idlcpblrng  14527  crngridl  14534  expghmap  14611  mulgghm2  14612  mulgrhm  14613  znf1o  14655  znleval  14657  znidom  14661  znidomb  14662  znunit  14663  mplsubgfilemcl  14703  iuncld  14829  ssnei2  14871  topssnei  14876  restopnb  14895  cnfval  14908  cnpfval  14909  iscnp4  14932  cnptopco  14936  cncnpi  14942  cncnp  14944  cnconst2  14947  cnrest2  14950  cnptoprest  14953  cnptoprest2  14954  cnpdis  14956  lmss  14960  lmtopcnp  14964  neitx  14982  txcnp  14985  txrest  14990  txdis1cn  14992  txlm  14993  cnmpt21  15005  imasnopn  15013  xmetres2  15093  blvalps  15102  blval  15103  elbl2ps  15106  elbl2  15107  blhalf  15122  blssexps  15143  blssex  15144  ssblex  15145  blin2  15146  bdmetval  15214  xmetxp  15221  xmettx  15224  metcnpi3  15231  txmetcnp  15232  addcncntoplem  15275  fsumcncntop  15281  elcncf2  15288  mulc1cncf  15303  cncfco  15305  cncfmet  15306  cncfmptc  15310  mulcncf  15322  dedekindeulemub  15332  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeu  15337  dedekindicclemub  15341  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemuopn  15352  dich0  15366  limcimo  15379  cnplimccntop  15384  limccnp2lem  15390  limccnp2cntop  15391  dvfvalap  15395  dveflem  15440  plycolemc  15472  plyco  15473  plyrecj  15477  reeff1olem  15485  reeff1oleme  15486  eflt  15489  sin0pilem2  15496  pilem3  15497  ioocosf1o  15568  cxplt  15630  cxple  15631  cxplt3  15634  apcxp2  15653  rprelogbmul  15669  rprelogbdiv  15671  logbgt0b  15680  logbgcd1irrap  15684  mpodvdsmulf1o  15704  fsumdvdsmul  15705  lgsdir2lem5  15751  lgsdi  15756  lgsne0  15757  gausslemma2dlem1f1o  15779  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem2  15801  lgsquad2  15802  2sqlem6  15839  2sqlem8  15842  2sqlem9  15843  2sqlem10  15844  upgredg  15983  usgredg4  16054  uspgredg2vlem  16059  usgr1eop  16084  vtxedgfi  16095  vtxlpfi  16096  iswlkg  16126  upgriswlkdc  16157  upgr2wlkdc  16172  clwwlkccatlem  16195  clwwlknonex2e  16235  nnti  16527  pwtrufal  16534  pwf1oexmid  16536  sssneq  16539  qdencn  16567  cvgcmp2n  16573  trilpolemlt1  16581  trirec0  16584  redc0  16597  reap0  16598  cndcap  16599  nconstwlpolemgt0  16604  neap0mkv  16609  supfz  16611  inffz  16612