Theorem simprl 529

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprl	|- ( ( ph /\ ( ps /\ ch ) ) -> ps )

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2	1	ad2antrl 490	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ps )

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:  simp1rl  1064  simp2rl  1068  simp3rl  1072  rmob  3078  disjiun  4024  reg3exmidlemwe  4611  0xp  4739  imainss  5081  iotam  5246  fvmptt  5649  fcof1o  5832  isotr  5859  riota5f  5898  ovmpodf  6050  unielxp  6227  fnmpoovd  6268  1stconst  6274  2ndconst  6275  cnvf1olem  6277  tfrlemi14d  6386  tfrexlem  6387  tfr1onlemres  6402  tfrcllemres  6415  tfrcldm  6416  frecabcl  6452  nnaordi  6561  swoer  6615  qliftfun  6671  ecopovsymg  6688  th3qlem1  6691  pw2f1odclem  6890  mapen  6902  mapxpen  6904  fidifsnen  6926  fisbth  6939  findcard2d  6947  findcard2sd  6948  diffisn  6949  diffifi  6950  ac6sfi  6954  fimax2gtri  6957  fientri3  6971  nnwetri  6972  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  fisseneq  6988  fidcenumlemrk  7013  fidcenumlemr  7014  isbth  7026  ordiso2  7094  difinfsnlem  7158  difinfinf  7160  ctmlemr  7167  ctssdccl  7170  fodjum  7205  fodju0  7206  omniwomnimkv  7226  exmidfodomrlemrALT  7263  netap  7314  exmidmotap  7321  cc1  7325  cc2lem  7326  cc3  7328  cc4f  7329  cc4n  7331  dfplpq2  7414  dfmpq2  7415  mulpipqqs  7433  distrnqg  7447  ltexnqq  7468  subhalfnqq  7474  distrnq0  7519  prarloclemup  7555  prarloclem3  7557  prarloc  7563  genplt2i  7570  nqprl  7611  nqpru  7612  prmuloc  7626  mullocpr  7631  distrlem4prl  7644  distrlem4pru  7645  ltaddpr  7657  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  ltaprlem  7678  ltaprg  7679  prplnqu  7680  addextpr  7681  recexprlemdisj  7690  recexprlemloc  7691  recexprlem1ssl  7693  aptiprleml  7699  aptiprlemu  7700  ltmprr  7702  archpr  7703  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlem1  7719  cauappcvgprlem2  7720  cauappcvgprlemlim  7721  caucvgprlemnkj  7726  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlem2  7740  caucvgprprlemnkltj  7749  caucvgprprlemnkeqj  7750  caucvgprprlemnjltk  7751  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemdisj  7762  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  caucvgprprlem2  7770  suplocexprlemrl  7777  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemex  7782  suplocexprlemub  7783  suplocexprlemlub  7784  recexgt0sr  7833  mulgt0sr  7838  prsrriota  7848  caucvgsrlemoffres  7860  suplocsrlem  7868  cnm  7892  addcnsr  7894  mulcnsr  7895  mulcnsrec  7903  axaddcl  7924  axmulcl  7926  axmulcom  7931  rereceu  7949  recriota  7950  axcaucvglemres  7959  axpre-suploclemres  7961  lelttr  8108  ltletr  8109  readdcan  8159  addcan  8199  addcan2  8200  addsub4  8262  ltadd2  8438  le2add  8463  lt2add  8464  lt2sub  8479  le2sub  8480  eqord1  8502  rimul  8604  rereim  8605  ltmul1  8611  apreim  8622  mulreim  8623  apcotr  8626  apadd1  8627  addext  8629  apneg  8630  mulext1  8631  mulext  8633  ltleap  8651  aprcl  8665  mulap0  8673  mulcanapd  8680  receuap  8688  recapb  8690  rec11ap  8729  rec11rap  8730  divdivdivap  8732  ddcanap  8745  divadddivap  8746  conjmulap  8748  subrecap  8858  prodgt0gt0  8870  prodge0  8873  ltmul12a  8879  lemulge11  8885  lt2mul2div  8898  ltrec  8902  lerec  8903  lt2msq  8905  lerec2  8908  le2msq  8920  msq11  8921  ledivp1  8922  mulle0r  8963  suprzclex  9415  peano5uzti  9425  supinfneg  9660  infsupneg  9661  qapne  9704  xrlelttr  9872  xrltletr  9873  xrre  9886  xaddge0  9944  xle2add  9945  xlt2add  9946  divelunit  10068  fzass4  10128  fzocatel  10266  exbtwnzlemex  10318  rebtwn2z  10323  qbtwnre  10325  modqid  10420  modqcyc  10430  modqaddabs  10433  modqaddmod  10434  mulqaddmodid  10435  modqadd2mod  10445  modqltm1p1mod  10447  modqsubmod  10453  modqsubmodmod  10454  modqmulmod  10460  modqmulmodr  10461  modqaddmulmod  10462  modqsubdir  10464  frec2uzisod  10478  iseqovex  10529  seqvalcd  10532  seq1g  10534  seqf  10535  seqovcd  10538  seqm1g  10545  seq3fveq2  10546  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  iseqf1olemnab  10572  seqf1oglem1  10590  seqf1og  10592  seq3id2  10597  seqhomog  10601  seq3distr  10603  expcl2lemap  10622  expnegzap  10644  ltexp2a  10662  le2sq2  10686  nn0ltexp2  10780  nn0opth2  10795  bcval5  10834  hashcl  10852  hashen  10855  fihashdom  10874  hashunlem  10875  hashun  10876  fimaxq  10898  zfz1isolem1  10911  zfz1iso  10912  lencl  10918  sswrd  10923  fstwrdne0  10953  cvg1nlemres  11129  cvg1n  11130  recvguniq  11139  resqrexlemp1rp  11150  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemex  11169  sqrtmul  11179  sqrtsq  11188  absexpzap  11224  absle  11233  abs3lem  11255  amgm2  11262  maxleastlt  11359  maxltsup  11362  fimaxre2  11370  xrmaxleastlt  11399  xrmaxltsup  11401  xrmaxaddlem  11403  climcn2  11452  addcn2  11453  mulcn2  11455  reccn2ap  11456  climcau  11490  summodclem2  11525  summodc  11526  fsumf1o  11533  fisumss  11535  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  fsum2dlemstep  11577  mptfzshft  11585  fsumrev  11586  fsummulc2  11591  modfsummod  11601  fsumrelem  11614  binom  11627  cvgratnn  11674  mertenslemub  11677  prodmodc  11721  zproddc  11722  fprodf1o  11731  fprodssdc  11733  fprodmul  11734  fprodrev  11762  fprod2dlemstep  11765  efcllem  11802  tanaddaplem  11881  dvdsval2  11933  moddvds  11942  dvdsabseq  11989  dvdsflip  11993  oexpneg  12018  fldivndvdslt  12076  zsupcllemstep  12082  zssinfcl  12085  suprzubdc  12089  zsupssdc  12091  suprzcl2dc  12092  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemeu  12144  dfgcd3  12147  bezout  12148  dvdsmulgcd  12162  bezoutr  12169  nninfctlemfo  12177  ialgrlem1st  12180  lcmgcdlem  12215  coprmdvds2  12231  qredeu  12235  rpdvds  12237  isprm5lem  12279  isprm6  12285  pw2dvdslemn  12303  nonsq  12345  crth  12362  eulerthlemh  12369  pclemdc  12426  pcprendvds2  12429  pceu  12433  pcval  12434  pczpre  12435  pcmul  12439  pcqmul  12441  pcqcl  12444  pcid  12462  pcneg  12463  pcgcd1  12466  pc2dvds  12468  pcprmpw2  12471  difsqpwdvds  12476  pcmpt  12481  pockthg  12495  1arith  12505  mul4sq  12532  4sqexercise2  12537  ennnfonelemg  12560  ennnfonelemex  12571  ennnfonelemrnh  12573  ennnfonelemrn  12576  ennnfonelemdm  12577  ennnfonelemnn0  12579  ennnfonelemim  12581  ennnfone  12582  ctinfomlemom  12584  ctinf  12587  ctiunctlemfo  12596  nninfdclemcl  12605  nninfdclemf  12606  nninfdclemp1  12607  unbendc  12611  isstruct2r  12629  setscom  12658  qusval  12906  ercpbl  12914  opifismgmdc  12954  grpinvalem  12968  grprida  12970  igsumvalx  12972  gsumfzval  12974  gsumpropd2  12976  gsumval2  12980  sgrppropd  12996  mndpropd  13021  issubmnd  13023  submnd0  13025  mhmf1o  13042  0mhm  13058  resmhm  13059  mhmco  13062  mhmima  13063  mhmeql  13064  gsumwsubmcl  13068  gsumfzcl  13071  grppropd  13089  grpinvid1  13124  grpinvid2  13125  grplcan  13134  grplmulf1o  13146  grpnpncan0  13168  dfgrp3mlem  13170  grplactcnv  13174  mulgval  13192  mulgfng  13194  mulg1  13199  mulgnnp1  13200  mulgneg  13210  mulgnndir  13221  mulgdirlem  13223  mulgnn0ass  13228  mulgass  13229  subgmulg  13258  issubg4m  13263  subgintm  13268  0nsg  13284  eqgcpbl  13298  ghmmulg  13326  ghmpreima  13336  ghmeql  13337  ghmnsgima  13338  ghmnsgpreima  13339  ghmf1  13343  ghmf1o  13345  conjghm  13346  conjnmzb  13350  qusghm  13352  ablpncan3  13387  invghm  13399  eqgabl  13400  qusecsub  13401  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  imasrng  13452  qusrng  13454  srglmhm  13489  srgrmhm  13490  ringpropd  13534  ringlghm  13557  ringrghm  13558  imasring  13560  qusring2  13562  opprrngbg  13574  dvdsrvald  13589  dvdsrd  13590  dvdsrex  13594  dvdsrtr  13597  unitgrp  13612  unitpropdg  13644  rhmopp  13672  isnzr2  13680  issubrng2  13706  subrngintm  13708  subrgintm  13739  rhmpropd  13750  aprap  13782  lmodprop2d  13844  rmodislmodlem  13846  lssvacl  13861  lssvsubcl  13862  lssvscl  13871  islss3  13875  lsspropdg  13927  rnglidlmcl  13976  2idlcpblrng  14019  crngridl  14026  expghmap  14095  mulgghm2  14096  mulgrhm  14097  znf1o  14139  znleval  14141  znidom  14145  psrval  14152  epttop  14258  topssnei  14330  restbasg  14336  restopnb  14349  cnfval  14362  cnpfval  14363  iscnp4  14386  cnpnei  14387  cnptopco  14390  cncnp  14398  cnrest2  14404  cnptoprest  14407  cnptoprest2  14408  lmss  14414  lmtopcnp  14418  neitx  14436  txcnp  14439  txrest  14444  txdis  14445  txlm  14447  cnmpt21  14459  imasnopn  14467  xmetres2  14547  blvalps  14556  blval  14557  bl2in  14571  blhalf  14576  blssps  14595  blss  14596  blssexps  14597  blssex  14598  ssblex  14599  blin2  14600  metss2lem  14665  bdmetval  14668  bdmopn  14672  metrest  14674  xmetxp  14675  xmetxpbl  14676  xmettx  14678  metcnp3  14679  txmetcnp  14686  addcncntoplem  14719  elcncf2  14729  mulc1cncf  14744  cncfco  14746  cncfmet  14747  mulcncf  14762  dedekindeulemub  14772  dedekindeulemloc  14773  dedekindeulemlu  14775  dedekindeu  14777  suplociccex  14779  dedekindicclemub  14781  dedekindicclemloc  14782  dedekindicclemlu  14784  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdec  14798  ivthreinc  14799  dich0  14806  limcimolemlt  14818  limcimo  14819  cnplimccntop  14824  limccnp2lem  14830  limccnp2cntop  14831  dvfvalap  14835  dveflem  14872  reeff1olem  14906  reeff1oleme  14907  eflt  14910  sin0pilem2  14917  pilem3  14918  ptolemy  14959  ioocosf1o  14989  cxplt  15050  cxple  15051  cxplt3  15054  apcxp2  15072  rprelogbmul  15087  rprelogbdiv  15089  logbgt0b  15098  logbgcd1irrap  15102  lgsdir2lem5  15148  lgsdir  15151  lgsdi  15153  lgsne0  15154  gausslemma2dlem1f1o  15176  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem6  15207  2sqlem10  15212  nnti  15485  pwtrufal  15488  pwf1oexmid  15490  sssneq  15492  qdencn  15517  cvgcmp2n  15523  trilpolemlt1  15531  trirec0  15534  trirec0xor  15535  redc0  15547  reap0  15548  cndcap  15549  nconstwlpolemgt0  15554  neap0mkv  15559  supfz  15561  inffz  15562