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  3090  disjiun  4038  reg3exmidlemwe  4625  0xp  4753  imainss  5095  iotam  5260  fvmptt  5665  fcof1o  5848  isotr  5875  riota5f  5914  ovmpodf  6067  unielxp  6250  fnmpoovd  6291  1stconst  6297  2ndconst  6298  cnvf1olem  6300  tfrlemi14d  6409  tfrexlem  6410  tfr1onlemres  6425  tfrcllemres  6438  tfrcldm  6439  frecabcl  6475  nnaordi  6584  swoer  6638  qliftfun  6694  ecopovsymg  6711  th3qlem1  6714  pw2f1odclem  6913  mapen  6925  mapxpen  6927  fidifsnen  6949  fisbth  6962  findcard2d  6970  findcard2sd  6971  diffisn  6972  diffifi  6973  ac6sfi  6977  fimax2gtri  6980  fientri3  6994  nnwetri  6995  unsnfi  6998  unsnfidcex  6999  unsnfidcel  7000  fisseneq  7013  fidcenumlemrk  7038  fidcenumlemr  7039  isbth  7051  ordiso2  7119  difinfsnlem  7183  difinfinf  7185  ctmlemr  7192  ctssdccl  7195  fodjum  7230  fodju0  7231  omniwomnimkv  7251  exmidfodomrlemrALT  7293  netap  7348  exmidmotap  7355  cc1  7359  cc2lem  7360  cc3  7362  cc4f  7363  cc4n  7365  dfplpq2  7449  dfmpq2  7450  mulpipqqs  7468  distrnqg  7482  ltexnqq  7503  subhalfnqq  7509  distrnq0  7554  prarloclemup  7590  prarloclem3  7592  prarloc  7598  genplt2i  7605  nqprl  7646  nqpru  7647  prmuloc  7661  mullocpr  7666  distrlem4prl  7679  distrlem4pru  7680  ltaddpr  7692  ltexprlemopl  7696  ltexprlemlol  7697  ltexprlemopu  7698  ltexprlemupu  7699  ltexprlemrl  7705  ltexprlemru  7707  addcanprleml  7709  addcanprlemu  7710  ltaprlem  7713  ltaprg  7714  prplnqu  7715  addextpr  7716  recexprlemdisj  7725  recexprlemloc  7726  recexprlem1ssl  7728  aptiprleml  7734  aptiprlemu  7735  ltmprr  7737  archpr  7738  cauappcvgprlemopl  7741  cauappcvgprlemopu  7743  cauappcvgprlemdisj  7746  cauappcvgprlemloc  7747  cauappcvgprlem1  7754  cauappcvgprlem2  7755  cauappcvgprlemlim  7756  caucvgprlemnkj  7761  caucvgprlemopl  7764  caucvgprlemopu  7766  caucvgprlemdisj  7769  caucvgprlemloc  7770  caucvgprlem2  7775  caucvgprprlemnkltj  7784  caucvgprprlemnkeqj  7785  caucvgprprlemnjltk  7786  caucvgprprlemmu  7790  caucvgprprlemopl  7792  caucvgprprlemopu  7794  caucvgprprlemdisj  7797  caucvgprprlemloc  7798  caucvgprprlemexbt  7801  caucvgprprlemaddq  7803  caucvgprprlem2  7805  suplocexprlemrl  7812  suplocexprlemmu  7813  suplocexprlemru  7814  suplocexprlemdisj  7815  suplocexprlemloc  7816  suplocexprlemex  7817  suplocexprlemub  7818  suplocexprlemlub  7819  recexgt0sr  7868  mulgt0sr  7873  prsrriota  7883  caucvgsrlemoffres  7895  suplocsrlem  7903  cnm  7927  addcnsr  7929  mulcnsr  7930  mulcnsrec  7938  axaddcl  7959  axmulcl  7961  axmulcom  7966  rereceu  7984  recriota  7985  axcaucvglemres  7994  axpre-suploclemres  7996  lelttr  8143  ltletr  8144  readdcan  8194  addcan  8234  addcan2  8235  addsub4  8297  ltadd2  8474  le2add  8499  lt2add  8500  lt2sub  8515  le2sub  8516  eqord1  8538  rimul  8640  rereim  8641  ltmul1  8647  apreim  8658  mulreim  8659  apcotr  8662  apadd1  8663  addext  8665  apneg  8666  mulext1  8667  mulext  8669  ltleap  8687  aprcl  8701  mulap0  8709  mulcanapd  8716  receuap  8724  recapb  8726  rec11ap  8765  rec11rap  8766  divdivdivap  8768  ddcanap  8781  divadddivap  8782  conjmulap  8784  subrecap  8894  prodgt0gt0  8906  prodge0  8909  ltmul12a  8915  lemulge11  8921  lt2mul2div  8934  ltrec  8938  lerec  8939  lt2msq  8941  lerec2  8944  le2msq  8956  msq11  8957  ledivp1  8958  mulle0r  8999  suprzclex  9453  peano5uzti  9463  supinfneg  9698  infsupneg  9699  qapne  9742  xrlelttr  9910  xrltletr  9911  xrre  9924  xaddge0  9982  xle2add  9983  xlt2add  9984  divelunit  10106  fzass4  10166  fzocatel  10309  zsupcllemstep  10353  zssinfcl  10356  suprzubdc  10360  zsupssdc  10362  suprzcl2dc  10363  exbtwnzlemex  10373  rebtwn2z  10378  qbtwnre  10380  modqid  10475  modqcyc  10485  modqaddabs  10488  modqaddmod  10489  mulqaddmodid  10490  modqadd2mod  10500  modqltm1p1mod  10502  modqsubmod  10508  modqsubmodmod  10509  modqmulmod  10515  modqmulmodr  10516  modqaddmulmod  10517  modqsubdir  10519  frec2uzisod  10533  iseqovex  10584  seqvalcd  10587  seq1g  10589  seqf  10590  seqovcd  10593  seqm1g  10600  seq3fveq2  10601  seq3shft2  10607  seqshft2g  10608  monoord  10611  seq3split  10614  seqsplitg  10615  iseqf1olemnab  10627  seqf1oglem1  10645  seqf1og  10647  seq3id2  10652  seqhomog  10656  seq3distr  10658  expcl2lemap  10677  expnegzap  10699  ltexp2a  10717  le2sq2  10741  nn0ltexp2  10835  nn0opth2  10850  bcval5  10889  hashcl  10907  hashen  10910  fihashdom  10929  hashunlem  10930  hashun  10931  fimaxq  10953  zfz1isolem1  10966  zfz1iso  10967  lencl  10973  sswrd  10978  fstwrdne0  11008  lswlgt0cl  11020  cvg1nlemres  11215  cvg1n  11216  recvguniq  11225  resqrexlemp1rp  11236  resqrexlemoverl  11251  resqrexlemglsq  11252  resqrexlemex  11255  sqrtmul  11265  sqrtsq  11274  absexpzap  11310  absle  11319  abs3lem  11341  amgm2  11348  maxleastlt  11445  maxltsup  11448  fimaxre2  11457  xrmaxleastlt  11486  xrmaxltsup  11488  xrmaxaddlem  11490  climcn2  11539  addcn2  11540  mulcn2  11542  reccn2ap  11543  climcau  11577  summodclem2  11612  summodc  11613  fsumf1o  11620  fisumss  11622  fsum3cvg3  11626  fsumcl2lem  11628  fsumadd  11636  fsum2dlemstep  11664  mptfzshft  11672  fsumrev  11673  fsummulc2  11678  modfsummod  11688  fsumrelem  11701  binom  11714  cvgratnn  11761  mertenslemub  11764  prodmodc  11808  zproddc  11809  fprodf1o  11818  fprodssdc  11820  fprodmul  11821  fprodrev  11849  fprod2dlemstep  11852  efcllem  11889  tanaddaplem  11968  dvdsval2  12020  moddvds  12029  dvdsabseq  12077  dvdsflip  12081  oexpneg  12107  fldivndvdslt  12167  bitsfi  12187  bezoutlemnewy  12236  bezoutlemstep  12237  bezoutlemeu  12247  dfgcd3  12250  bezout  12251  dvdsmulgcd  12265  bezoutr  12272  nninfctlemfo  12280  ialgrlem1st  12283  lcmgcdlem  12318  coprmdvds2  12334  qredeu  12338  rpdvds  12340  isprm5lem  12382  isprm6  12388  pw2dvdslemn  12406  nonsq  12448  crth  12465  eulerthlemh  12472  pclemdc  12530  pcprendvds2  12533  pceu  12537  pcval  12538  pczpre  12539  pcmul  12543  pcqmul  12545  pcqcl  12548  pcid  12566  pcneg  12567  pcgcd1  12570  pc2dvds  12572  pcprmpw2  12575  difsqpwdvds  12580  pcmpt  12585  pockthg  12599  1arith  12609  mul4sq  12636  4sqexercise2  12641  ennnfonelemg  12693  ennnfonelemex  12704  ennnfonelemrnh  12706  ennnfonelemrn  12709  ennnfonelemdm  12710  ennnfonelemnn0  12712  ennnfonelemim  12714  ennnfone  12715  ctinfomlemom  12717  ctinf  12720  ctiunctlemfo  12729  nninfdclemcl  12738  nninfdclemf  12739  nninfdclemp1  12740  unbendc  12744  isstruct2r  12762  setscom  12791  qusval  13073  ercpbl  13081  opifismgmdc  13121  grpinvalem  13135  grprida  13137  igsumvalx  13139  gsumfzval  13141  gsumpropd2  13143  gsumval2  13147  sgrppropd  13163  prdssgrpd  13165  mndpropd  13190  issubmnd  13192  submnd0  13194  prdsmndd  13198  mhmf1o  13220  0mhm  13236  resmhm  13237  mhmco  13240  mhmima  13241  mhmeql  13242  gsumwsubmcl  13246  gsumfzcl  13249  grppropd  13267  grpinvid1  13302  grpinvid2  13303  grplcan  13312  grplmulf1o  13324  grpnpncan0  13346  dfgrp3mlem  13348  grplactcnv  13352  pwssub  13363  mulgval  13376  mulgfng  13378  mulg1  13383  mulgnnp1  13384  mulgneg  13394  mulgnndir  13405  mulgdirlem  13407  mulgnn0ass  13412  mulgass  13413  subgmulg  13442  issubg4m  13447  subgintm  13452  0nsg  13468  eqgcpbl  13482  ghmmulg  13510  ghmpreima  13520  ghmeql  13521  ghmnsgima  13522  ghmnsgpreima  13523  ghmf1  13527  ghmf1o  13529  conjghm  13530  conjnmzb  13534  qusghm  13536  ablpncan3  13571  invghm  13583  eqgabl  13584  qusecsub  13585  gsumfzreidx  13591  gsumfzsubmcl  13592  gsumfzmptfidmadd  13593  gsumfzmhm  13597  imasrng  13636  qusrng  13638  srglmhm  13673  srgrmhm  13674  ringpropd  13718  ringlghm  13741  ringrghm  13742  imasring  13744  qusring2  13746  opprrngbg  13758  dvdsrvald  13773  dvdsrd  13774  dvdsrex  13778  dvdsrtr  13781  unitgrp  13796  unitpropdg  13828  rhmopp  13856  isnzr2  13864  issubrng2  13890  subrngintm  13892  subrgintm  13923  rhmpropd  13934  aprap  13966  lmodprop2d  14028  rmodislmodlem  14030  lssvacl  14045  lssvsubcl  14046  lssvscl  14055  islss3  14059  lsspropdg  14111  rnglidlmcl  14160  2idlcpblrng  14203  crngridl  14210  expghmap  14287  mulgghm2  14288  mulgrhm  14289  znf1o  14331  znleval  14333  znidom  14337  psrval  14346  mplsubgfilemcl  14379  epttop  14480  topssnei  14552  restbasg  14558  restopnb  14571  cnfval  14584  cnpfval  14585  iscnp4  14608  cnpnei  14609  cnptopco  14612  cncnp  14620  cnrest2  14626  cnptoprest  14629  cnptoprest2  14630  lmss  14636  lmtopcnp  14640  neitx  14658  txcnp  14661  txrest  14666  txdis  14667  txlm  14669  cnmpt21  14681  imasnopn  14689  xmetres2  14769  blvalps  14778  blval  14779  bl2in  14793  blhalf  14798  blssps  14817  blss  14818  blssexps  14819  blssex  14820  ssblex  14821  blin2  14822  metss2lem  14887  bdmetval  14890  bdmopn  14894  metrest  14896  xmetxp  14897  xmetxpbl  14898  xmettx  14900  metcnp3  14901  txmetcnp  14908  addcncntoplem  14951  elcncf2  14964  mulc1cncf  14979  cncfco  14981  cncfmet  14982  mulcncf  14998  dedekindeulemub  15008  dedekindeulemloc  15009  dedekindeulemlu  15011  dedekindeu  15013  suplociccex  15015  dedekindicclemub  15017  dedekindicclemloc  15018  dedekindicclemlu  15020  dedekindicc  15023  ivthinclemlopn  15026  ivthinclemuopn  15028  ivthdec  15034  ivthreinc  15035  dich0  15042  limcimolemlt  15054  limcimo  15055  cnplimccntop  15060  limccnp2lem  15066  limccnp2cntop  15067  dvfvalap  15071  dvmptfsum  15115  dveflem  15116  plyco  15149  plycn  15152  plyrecj  15153  reeff1olem  15161  reeff1oleme  15162  eflt  15165  sin0pilem2  15172  pilem3  15173  ptolemy  15214  ioocosf1o  15244  cxplt  15306  cxple  15307  cxplt3  15310  apcxp2  15329  rprelogbmul  15345  rprelogbdiv  15347  logbgt0b  15356  logbgcd1irrap  15360  fsumdvdsmul  15381  perfectlem2  15390  lgsdir2lem5  15427  lgsdir  15430  lgsdi  15432  lgsne0  15433  gausslemma2dlem1f1o  15455  lgseisenlem2  15466  lgsquadlem1  15472  lgsquadlem2  15473  lgsquad2lem2  15477  lgsquad2  15478  2sqlem6  15515  2sqlem10  15520  nnti  15793  pwtrufal  15798  pwf1oexmid  15800  sssneq  15803  qdencn  15830  cvgcmp2n  15836  trilpolemlt1  15844  trirec0  15847  trirec0xor  15848  redc0  15860  reap0  15861  cndcap  15862  nconstwlpolemgt0  15867  neap0mkv  15872  supfz  15874  inffz  15875