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  6609  tfrexlem  6610  tfr1onlemres  6625  tfrcllemres  6638  tfrcldm  6639  frecabcl  6675  nnaordi  6786  swoer  6840  qliftfun  6896  ecopovsymg  6913  th3qlem1  6916  pw2f1odclem  7140  mapen  7152  mapxpen  7154  fidifsnen  7178  fisbth  7193  findcard2d  7201  findcard2sd  7202  diffisn  7203  diffifi  7204  ac6sfi  7208  fidcen  7209  fimax2gtri  7212  fientri3  7228  nnwetri  7229  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  fisseneq  7248  exmidssfi  7252  fidcenumlemrk  7278  fidcenumlemr  7279  isbth  7291  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  9754  peano5uzti  9764  supinfneg  10010  infsupneg  10011  qapne  10054  xrlelttr  10224  xrltletr  10225  xrre  10238  xaddge0  10296  xle2add  10297  xlt2add  10298  divelunit  10420  fzass4  10484  fzocatel  10633  zsupcllemstep  10678  zssinfcl  10681  infssfzcldc  10685  infssfzledc  10686  suprzubdc  10687  zsupssdc  10689  suprzcl2dc  10690  exbtwnzlemex  10700  rebtwn2z  10705  qbtwnre  10707  modqid  10806  modqcyc  10816  modqaddabs  10819  modqaddmod  10820  mulqaddmodid  10821  modqadd2mod  10831  modqltm1p1mod  10833  modqsubmod  10839  modqsubmodmod  10840  modqmulmod  10846  modqmulmodr  10847  modqaddmulmod  10848  modqsubdir  10850  frec2uzisod  10864  iseqovex  10915  seqvalcd  10918  seq1g  10920  seqf  10921  seqovcd  10924  seqm1g  10931  seq3fveq2  10932  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  iseqf1olemnab  10958  seqf1oglem1  10976  seqf1og  10978  seq3id2  10983  seqhomog  10987  seq3distr  10989  expcl2lemap  11008  expnegzap  11030  ltexp2a  11048  le2sq2  11072  nn0ltexp2  11168  nn0opth2  11183  bcval5  11222  hashcl  11241  hashen  11244  fihashdom  11264  hashunlem  11265  hashun  11266  hashmap  11289  fimaxq  11291  hashfibclem  11303  hashfibc  11304  hashf1lem1  11306  hashf1lem2  11307  hashf1  11308  zfz1isolem1  11313  zfz1iso  11314  lencl  11329  sswrd  11334  fstwrdne0  11365  lswlgt0cl  11378  ccatw2s1p1g  11434  ccat2s1fstg  11437  swrdval  11441  wrdind  11515  wrd2ind  11516  swrdccatfn  11517  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12  11526  pfxccat3a  11531  reuccatpfxs1  11540  cvg1nlemres  11772  cvg1n  11773  recvguniq  11782  resqrexlemp1rp  11793  resqrexlemoverl  11808  resqrexlemglsq  11809  resqrexlemex  11812  sqrtmul  11822  sqrtsq  11831  absexpzap  11868  absle  11877  abs3lem  11899  amgm2  11906  maxleastlt  12003  maxltsup  12006  fimaxre2  12015  fiidxsupcl  12017  xrmaxleastlt  12046  xrmaxltsup  12048  xrmaxaddlem  12050  climcn2  12099  addcn2  12100  mulcn2  12102  reccn2ap  12103  climcau  12137  summodclem2  12173  summodc  12174  fsumf1o  12181  fisumss  12183  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  fsum2dlemstep  12225  mptfzshft  12233  fsumrev  12234  fsummulc2  12239  modfsummod  12249  fsumrelem  12262  binom  12275  cvgratnn  12322  mertenslemub  12325  prodmodc  12369  zproddc  12370  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  fprodrev  12410  fprod2dlemstep  12413  efcllem  12450  tanaddaplem  12529  dvdsval2  12581  moddvds  12590  dvdsabseq  12638  dvdsflip  12642  oexpneg  12668  fldivndvdslt  12728  bitsfi  12748  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemeu  12808  dfgcd3  12811  bezout  12812  dvdsmulgcd  12826  bezoutr  12833  nninfctlemfo  12841  ialgrlem1st  12844  lcmgcdlem  12879  coprmdvds2  12895  qredeu  12899  rpdvds  12901  isprm5lem  12944  isprm6  12950  pwbdvdslemn  12968  nnmaxpwlemparts  12976  nonsq  13011  crth  13030  eulerthlemh  13037  pclemdc  13095  pcprendvds2  13098  pceu  13102  pcval  13103  pczpre  13104  pcmul  13108  pcqmul  13110  pcqcl  13113  pcid  13131  pcneg  13132  pcgcd1  13135  pc2dvds  13137  pcprmpw2  13140  difsqpwdvds  13145  pcmpt  13150  pockthg  13164  1arith  13174  mul4sq  13201  4sqexercise2  13206  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemg  13351  ennnfonelemex  13362  ennnfonelemrnh  13364  ennnfonelemrn  13367  ennnfonelemdm  13368  ennnfonelemnn0  13370  ennnfonelemim  13372  ennnfone  13373  ctinfomlemom  13375  ctinf  13378  ctiunctlemfo  13387  nninfdclemcl  13396  nninfdclemf  13397  nninfdclemp1  13398  unbendc  13402  isstruct2r  13420  setscom  13449  qusval  13702  ercpbl  13710  opifismgmdc  13749  grpinvalem  13763  grprida  13765  gzsumvalx  13767  gzsumfzval  13769  gzsumval2  13772  sgrppropd  13786  mndpropd  13811  issubmnd  13813  submnd0  13815  mhmf1o  13835  0mhm  13851  resmhm  13852  mhmco  13855  mhmima  13856  mhmeql  13857  gzsumwsubmcl  13859  gzsumcl  13862  grppropd  13880  grpinvid1  13915  grpinvid2  13916  grplcan  13925  grplmulf1o  13937  grpnpncan0  13959  dfgrp3mlem  13961  grplactcnv  13965  mulgval  13983  mulgfng  13985  mulg1  13990  mulgnnp1  13991  mulgneg  14001  mulgnndir  14012  mulgdirlem  14014  mulgnn0ass  14019  mulgass  14020  subgmulg  14049  issubg4m  14054  subgintm  14059  0nsg  14075  eqgcpbl  14089  ghmmulg  14117  ghmpreima  14127  ghmeql  14128  ghmnsgima  14129  ghmnsgpreima  14130  ghmf1  14134  ghmf1o  14136  conjghm  14137  conjnmzb  14141  qusghm  14143  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  cntrsubgnsg  14174  cmnsubm  14201  ablpncan3  14210  invghm  14222  eqgabl  14223  qusecsub  14224  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gsumvalfi  14241  gsumclfi  14248  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumresfi  14262  gsum2dfilem2  14271  gsum2d2fi  14273  prdssgrpd  14297  prdsmndd  14300  pwssub  14322  imasrng  14361  qusrng  14363  srglmhm  14403  srgrmhm  14404  ringpropd  14449  ringlghm  14472  ringrghm  14473  imasring  14477  qusring2  14479  opprrngbg  14491  dvdsrvald  14508  dvdsrd  14509  dvdsrex  14513  dvdsrtr  14516  unitgrp  14531  unitpropdg  14563  rhmopp  14591  isnzr2  14599  issubrng2  14626  subrngintm  14628  subrgintm  14659  rhmpropd  14670  ringunitap  14701  aprap  14706  drngunitap  14716  lmodprop2d  14793  rmodislmodlem  14795  lssvacl  14810  lssvsubcl  14811  lssvscl  14820  islss3  14824  lsspropdg  14876  rnglidlmcl  14925  2idlcpblrng  14968  crngridl  14975  gsumfsum  15031  expghmap  15050  mulgghm2  15051  mulgrhm  15052  znf1o  15094  znleval  15096  znidom  15100  issubassa3  15120  assapropd  15122  asclghm  15133  issubassa2  15143  psrval  15160  psrbagcon  15174  psrbaglefifi  15175  psrbagconf1o  15177  psrbagmaxlem1  15178  psrbagmax  15183  gsumbagdiaglem  15184  gsumbagdiagfi  15185  psrass1filem  15186  mplsubgfilemcl  15232  epttop  15333  topssnei  15405  restbasg  15411  restopnb  15424  cnfval  15437  cnpfval  15438  iscnp4  15461  cnpnei  15462  cnptopco  15465  cncnp  15473  cnrest2  15479  cnptoprest  15482  cnptoprest2  15483  lmss  15489  lmtopcnp  15493  neitx  15511  txcnp  15514  txrest  15519  txdis  15520  txlm  15522  cnmpt21  15534  imasnopn  15542  xmetres2  15622  blvalps  15631  blval  15632  bl2in  15646  blhalf  15651  blssps  15670  blss  15671  blssexps  15672  blssex  15673  ssblex  15674  blin2  15675  metss2lem  15740  bdmetval  15743  bdmopn  15747  metrest  15749  xmetxp  15750  xmetxpbl  15751  xmettx  15753  metcnp3  15754  txmetcnp  15761  addcncntoplem  15804  elcncf2  15817  mulc1cncf  15832  cncfco  15834  cncfmet  15835  mulcncf  15851  dedekindeulemub  15861  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeu  15866  suplociccex  15868  dedekindicclemub  15870  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthdec  15887  ivthreinc  15888  dich0  15895  limcimolemlt  15907  limcimo  15908  cnplimccntop  15913  limccnp2lem  15919  limccnp2cntop  15920  dvfvalap  15924  dvmptfsum  15968  dveflem  15969  plyco  16002  plycn  16005  plyrecj  16006  reeff1olem  16014  reeff1oleme  16015  eflt  16018  sin0pilem2  16026  pilem3  16027  ptolemy  16068  ioocosf1o  16099  logdivlt  16141  logdivle  16142  rpcxpmul2z  16165  cxplt  16168  cxple  16169  cxplt3  16172  apcxp2  16191  rprelogbmul  16208  rprelogbdiv  16210  logbgt0b  16219  logbgcd1irrap  16223  zprmlogbap  16235  pellexlem3  16248  efnnfsumcl  16256  ppinprm  16277  chtnprm  16279  efchtqdvds  16282  fsumdvdsmul  16302  chtublem  16312  perfectlem2  16317  bposlem3  16330  lgsdir2lem5  16373  lgsdir  16376  lgsdi  16378  lgsne0  16379  gausslemma2dlem1f1o  16401  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  lgsquad2  16424  2sqlem6  16461  2sqlem10  16466  upgredg  16607  uhgrissubgr  16724  subgrprop3  16725  upgrspanop  16746  umgrspanop  16747  usgrspanop  16748  vtxedgfi  16752  vtxlpfi  16753  upgr2wlkdc  16840  clwwlkccatlem  16863  eupth2lemsfi  16941  depindlem3  16971  nnti  17244  pwtrufal  17249  pwf1oexmid  17251  sssneq  17254  qdencn  17295  cvgcmp2n  17305  trilpolemlt1  17314  trirec0  17317  trirec0xor  17318  qdiff  17322  redc0  17331  reap0  17332  cndcap  17333  nconstwlpolemgt0  17338  neap0mkv  17343  supfz  17345  inffz  17346