Theorem simprl 535

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 494	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ps )

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  simp1rl  1093  simp2rl  1097  simp3rl  1101  rmob  3145  elpr2elpr  3901  disjiun  4125  reg3exmidlemwe  4728  opabssxpd  4813  0xp  4857  imainss  5206  iotam  5372  fvmptt  5800  fcof1o  5998  isotr  6025  riota5f  6068  ovmpodf  6223  unielxp  6412  fnmpoovd  6455  1stconst  6461  2ndconst  6462  cnvf1olem  6464  fvn0elsupp  6495  suppcofn  6510  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemres  6624  tfrcllemres  6637  tfrcldm  6638  frecabcl  6674  nnaordi  6785  swoer  6839  qliftfun  6895  ecopovsymg  6912  th3qlem1  6915  pw2f1odclem  7138  mapen  7150  mapxpen  7152  fidifsnen  7176  fisbth  7191  findcard2d  7199  findcard2sd  7200  diffisn  7201  diffifi  7202  ac6sfi  7206  fidcen  7207  fimax2gtri  7210  fientri3  7226  nnwetri  7227  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  fisseneq  7246  exmidssfi  7250  fidcenumlemrk  7276  fidcenumlemr  7277  isbth  7289  ordiso2  7381  difinfsnlem  7445  difinfinf  7447  ctmlemr  7454  ctssdccl  7457  fodjum  7492  fodju0  7493  omniwomnimkv  7513  exmidfodomrlemrALT  7561  netap  7626  exmidmotap  7633  cc1  7637  cc2lem  7638  cc3  7640  cc4f  7641  cc4n  7643  dfplpq2  7727  dfmpq2  7728  mulpipqqs  7746  distrnqg  7760  ltexnqq  7781  subhalfnqq  7787  distrnq0  7832  prarloclemup  7868  prarloclem3  7870  prarloc  7876  genplt2i  7883  nqprl  7924  nqpru  7925  prmuloc  7939  mullocpr  7944  distrlem4prl  7957  distrlem4pru  7958  ltaddpr  7970  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  ltaprlem  7991  ltaprg  7992  prplnqu  7993  addextpr  7994  recexprlemdisj  8003  recexprlemloc  8004  recexprlem1ssl  8006  aptiprleml  8012  aptiprlemu  8013  ltmprr  8015  archpr  8016  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlem1  8032  cauappcvgprlem2  8033  cauappcvgprlemlim  8034  caucvgprlemnkj  8039  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlem2  8053  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemopu  8072  caucvgprprlemdisj  8075  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem2  8083  suplocexprlemrl  8090  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  recexgt0sr  8146  mulgt0sr  8151  prsrriota  8161  caucvgsrlemoffres  8173  suplocsrlem  8181  cnm  8205  addcnsr  8207  mulcnsr  8208  mulcnsrec  8216  axaddcl  8237  axmulcl  8239  axmulcom  8244  rereceu  8262  recriota  8263  axcaucvglemres  8272  axpre-suploclemres  8274  lelttr  8420  ltletr  8421  readdcan  8473  addcan  8513  addcan2  8514  addsub4  8576  ltadd2  8754  le2add  8779  lt2add  8780  lt2sub  8795  le2sub  8796  eqord1  8818  rimul  8921  rereim  8922  ltmul1  8928  apreim  8939  mulreim  8940  apcotr  8943  apadd1  8944  addext  8946  apneg  8947  mulext1  8948  mulext  8950  ltleap  8968  aprcl  8982  mulap0  8990  mulcanapd  8997  receuap  9007  recapb  9009  rec11ap  9048  rec11rap  9049  divdivdivap  9051  ddcanap  9064  divadddivap  9065  conjmulap  9067  subrecap  9177  prodgt0gt0  9189  prodge0  9192  ltmul12a  9198  lemulge11  9204  lt2mul2div  9217  ltrec  9221  lerec  9222  lt2msq  9224  lerec2  9227  le2msq  9239  msq11  9240  ledivp1  9241  mulle0r  9282  suprzclex  9755  peano5uzti  9765  supinfneg  10011  infsupneg  10012  qapne  10055  xrlelttr  10225  xrltletr  10226  xrre  10239  xaddge0  10297  xle2add  10298  xlt2add  10299  divelunit  10421  fzass4  10485  fzocatel  10634  zsupcllemstep  10679  zssinfcl  10682  infssfzcldc  10686  infssfzledc  10687  suprzubdc  10688  zsupssdc  10690  suprzcl2dc  10691  exbtwnzlemex  10701  rebtwn2z  10706  qbtwnre  10708  modqid  10807  modqcyc  10817  modqaddabs  10820  modqaddmod  10821  mulqaddmodid  10822  modqadd2mod  10832  modqltm1p1mod  10834  modqsubmod  10840  modqsubmodmod  10841  modqmulmod  10847  modqmulmodr  10848  modqaddmulmod  10849  modqsubdir  10851  frec2uzisod  10865  iseqovex  10916  seqvalcd  10919  seq1g  10921  seqf  10922  seqovcd  10925  seqm1g  10932  seq3fveq2  10933  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  iseqf1olemnab  10959  seqf1oglem1  10977  seqf1og  10979  seq3id2  10984  seqhomog  10988  seq3distr  10990  expcl2lemap  11009  expnegzap  11031  ltexp2a  11049  le2sq2  11073  nn0ltexp2  11169  nn0opth2  11184  bcval5  11223  hashcl  11242  hashen  11245  fihashdom  11265  hashunlem  11266  hashun  11267  hashmap  11290  fimaxq  11292  hashfibclem  11304  hashfibc  11305  hashf1lem1  11307  hashf1lem2  11308  hashf1  11309  zfz1isolem1  11314  zfz1iso  11315  lencl  11330  sswrd  11335  fstwrdne0  11366  lswlgt0cl  11379  ccatw2s1p1g  11435  ccat2s1fstg  11438  swrdval  11442  wrdind  11516  wrd2ind  11517  swrdccatfn  11518  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12  11527  pfxccat3a  11532  reuccatpfxs1  11541  cvg1nlemres  11773  cvg1n  11774  recvguniq  11783  resqrexlemp1rp  11794  resqrexlemoverl  11809  resqrexlemglsq  11810  resqrexlemex  11813  sqrtmul  11823  sqrtsq  11832  absexpzap  11869  absle  11878  abs3lem  11900  amgm2  11907  maxleastlt  12004  maxltsup  12007  fimaxre2  12016  fiidxsupcl  12018  xrmaxleastlt  12047  xrmaxltsup  12049  xrmaxaddlem  12051  climcn2  12100  addcn2  12101  mulcn2  12103  reccn2ap  12104  climcau  12138  summodclem2  12174  summodc  12175  fsumf1o  12182  fisumss  12184  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  fsum2dlemstep  12226  mptfzshft  12234  fsumrev  12235  fsummulc2  12240  modfsummod  12250  fsumrelem  12263  binom  12276  cvgratnn  12323  mertenslemub  12326  prodmodc  12370  zproddc  12371  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  fprodrev  12411  fprod2dlemstep  12414  efcllem  12451  tanaddaplem  12530  dvdsval2  12582  moddvds  12591  dvdsabseq  12639  dvdsflip  12643  oexpneg  12669  fldivndvdslt  12729  bitsfi  12749  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemeu  12809  dfgcd3  12812  bezout  12813  dvdsmulgcd  12827  bezoutr  12834  nninfctlemfo  12842  ialgrlem1st  12845  lcmgcdlem  12880  coprmdvds2  12896  qredeu  12900  rpdvds  12902  isprm5lem  12945  isprm6  12951  pwbdvdslemn  12969  nnmaxpwlemparts  12977  nonsq  13012  crth  13031  eulerthlemh  13038  pclemdc  13096  pcprendvds2  13099  pceu  13103  pcval  13104  pczpre  13105  pcmul  13109  pcqmul  13111  pcqcl  13114  pcid  13132  pcneg  13133  pcgcd1  13136  pc2dvds  13138  pcprmpw2  13141  difsqpwdvds  13146  pcmpt  13151  pockthg  13165  1arith  13175  mul4sq  13202  4sqexercise2  13207  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemg  13352  ennnfonelemex  13363  ennnfonelemrnh  13365  ennnfonelemrn  13368  ennnfonelemdm  13369  ennnfonelemnn0  13371  ennnfonelemim  13373  ennnfone  13374  ctinfomlemom  13376  ctinf  13379  ctiunctlemfo  13388  nninfdclemcl  13397  nninfdclemf  13398  nninfdclemp1  13399  unbendc  13403  isstruct2r  13421  setscom  13450  qusval  13703  ercpbl  13711  opifismgmdc  13750  grpinvalem  13764  grprida  13766  gzsumvalx  13768  gzsumfzval  13770  gzsumval2  13773  sgrppropd  13787  mndpropd  13812  issubmnd  13814  submnd0  13816  mhmf1o  13836  0mhm  13852  resmhm  13853  mhmco  13856  mhmima  13857  mhmeql  13858  gzsumwsubmcl  13860  gzsumcl  13863  grppropd  13881  grpinvid1  13916  grpinvid2  13917  grplcan  13926  grplmulf1o  13938  grpnpncan0  13960  dfgrp3mlem  13962  grplactcnv  13966  mulgval  13984  mulgfng  13986  mulg1  13991  mulgnnp1  13992  mulgneg  14002  mulgnndir  14013  mulgdirlem  14015  mulgnn0ass  14020  mulgass  14021  subgmulg  14050  issubg4m  14055  subgintm  14060  0nsg  14076  eqgcpbl  14090  ghmmulg  14118  ghmpreima  14128  ghmeql  14129  ghmnsgima  14130  ghmnsgpreima  14131  ghmf1  14135  ghmf1o  14137  conjghm  14138  conjnmzb  14142  qusghm  14144  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cntrsubgnsg  14175  cmnsubm  14202  ablpncan3  14211  invghm  14223  eqgabl  14224  qusecsub  14225  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gsumvalfi  14242  gsumclfi  14249  gsummptfidmadd  14251  gsumsubmclfi  14253  gsummptfidmsplit  14254  gsumresfi  14263  gsum2dfilem2  14272  gsum2d2fi  14274  prdssgrpd  14298  prdsmndd  14301  pwssub  14323  imasrng  14362  qusrng  14364  srglmhm  14404  srgrmhm  14405  ringpropd  14450  ringlghm  14473  ringrghm  14474  imasring  14478  qusring2  14480  opprrngbg  14492  dvdsrvald  14509  dvdsrd  14510  dvdsrex  14514  dvdsrtr  14517  unitgrp  14532  unitpropdg  14564  rhmopp  14592  isnzr2  14600  issubrng2  14627  subrngintm  14629  subrgintm  14660  rhmpropd  14671  ringunitap  14702  aprap  14707  drngunitap  14717  lmodprop2d  14794  rmodislmodlem  14796  lssvacl  14811  lssvsubcl  14812  lssvscl  14821  islss3  14825  lsspropdg  14877  rnglidlmcl  14926  2idlcpblrng  14969  crngridl  14976  gsumfsum  15032  expghmap  15051  mulgghm2  15052  mulgrhm  15053  znf1o  15095  znleval  15097  znidom  15101  issubassa3  15121  assapropd  15123  asclghm  15134  issubassa2  15144  psrval  15159  psrbagcon  15171  psrbaglefifi  15172  psrbagconf1o  15174  gsumbagdiaglem  15175  gsumbagdiagfi  15176  psrass1filem  15177  mplsubgfilemcl  15215  epttop  15316  topssnei  15388  restbasg  15394  restopnb  15407  cnfval  15420  cnpfval  15421  iscnp4  15444  cnpnei  15445  cnptopco  15448  cncnp  15456  cnrest2  15462  cnptoprest  15465  cnptoprest2  15466  lmss  15472  lmtopcnp  15476  neitx  15494  txcnp  15497  txrest  15502  txdis  15503  txlm  15505  cnmpt21  15517  imasnopn  15525  xmetres2  15605  blvalps  15614  blval  15615  bl2in  15629  blhalf  15634  blssps  15653  blss  15654  blssexps  15655  blssex  15656  ssblex  15657  blin2  15658  metss2lem  15723  bdmetval  15726  bdmopn  15730  metrest  15732  xmetxp  15733  xmetxpbl  15734  xmettx  15736  metcnp3  15737  txmetcnp  15744  addcncntoplem  15787  elcncf2  15800  mulc1cncf  15815  cncfco  15817  cncfmet  15818  mulcncf  15834  dedekindeulemub  15844  dedekindeulemloc  15845  dedekindeulemlu  15847  dedekindeu  15849  suplociccex  15851  dedekindicclemub  15853  dedekindicclemloc  15854  dedekindicclemlu  15856  dedekindicc  15859  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthdec  15870  ivthreinc  15871  dich0  15878  limcimolemlt  15890  limcimo  15891  cnplimccntop  15896  limccnp2lem  15902  limccnp2cntop  15903  dvfvalap  15907  dvmptfsum  15951  dveflem  15952  plyco  15985  plycn  15988  plyrecj  15989  reeff1olem  15997  reeff1oleme  15998  eflt  16001  sin0pilem2  16009  pilem3  16010  ptolemy  16051  ioocosf1o  16082  logdivlt  16124  logdivle  16125  rpcxpmul2z  16148  cxplt  16151  cxple  16152  cxplt3  16155  apcxp2  16174  rprelogbmul  16191  rprelogbdiv  16193  logbgt0b  16202  logbgcd1irrap  16206  zprmlogbap  16218  pellexlem3  16231  efnnfsumcl  16239  ppinprm  16260  chtnprm  16262  efchtqdvds  16265  fsumdvdsmul  16285  chtublem  16295  perfectlem2  16300  bposlem3  16313  lgsdir2lem5  16356  lgsdir  16359  lgsdi  16361  lgsne0  16362  gausslemma2dlem1f1o  16384  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  lgsquad2  16407  2sqlem6  16444  2sqlem10  16449  upgredg  16590  uhgrissubgr  16707  subgrprop3  16708  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  vtxedgfi  16735  vtxlpfi  16736  upgr2wlkdc  16823  clwwlkccatlem  16846  eupth2lemsfi  16924  depindlem3  16954  nnti  17227  pwtrufal  17232  pwf1oexmid  17234  sssneq  17237  qdencn  17278  cvgcmp2n  17288  trilpolemlt1  17297  trirec0  17300  trirec0xor  17301  qdiff  17305  redc0  17314  reap0  17315  cndcap  17316  nconstwlpolemgt0  17321  neap0mkv  17326  supfz  17328  inffz  17329