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  3082  disjiun  4028  reg3exmidlemwe  4615  0xp  4743  imainss  5085  iotam  5250  fvmptt  5653  fcof1o  5836  isotr  5863  riota5f  5902  ovmpodf  6054  unielxp  6232  fnmpoovd  6273  1stconst  6279  2ndconst  6280  cnvf1olem  6282  tfrlemi14d  6391  tfrexlem  6392  tfr1onlemres  6407  tfrcllemres  6420  tfrcldm  6421  frecabcl  6457  nnaordi  6566  swoer  6620  qliftfun  6676  ecopovsymg  6693  th3qlem1  6696  pw2f1odclem  6895  mapen  6907  mapxpen  6909  fidifsnen  6931  fisbth  6944  findcard2d  6952  findcard2sd  6953  diffisn  6954  diffifi  6955  ac6sfi  6959  fimax2gtri  6962  fientri3  6976  nnwetri  6977  unsnfi  6980  unsnfidcex  6981  unsnfidcel  6982  fisseneq  6995  fidcenumlemrk  7020  fidcenumlemr  7021  isbth  7033  ordiso2  7101  difinfsnlem  7165  difinfinf  7167  ctmlemr  7174  ctssdccl  7177  fodjum  7212  fodju0  7213  omniwomnimkv  7233  exmidfodomrlemrALT  7270  netap  7321  exmidmotap  7328  cc1  7332  cc2lem  7333  cc3  7335  cc4f  7336  cc4n  7338  dfplpq2  7421  dfmpq2  7422  mulpipqqs  7440  distrnqg  7454  ltexnqq  7475  subhalfnqq  7481  distrnq0  7526  prarloclemup  7562  prarloclem3  7564  prarloc  7570  genplt2i  7577  nqprl  7618  nqpru  7619  prmuloc  7633  mullocpr  7638  distrlem4prl  7651  distrlem4pru  7652  ltaddpr  7664  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  ltaprlem  7685  ltaprg  7686  prplnqu  7687  addextpr  7688  recexprlemdisj  7697  recexprlemloc  7698  recexprlem1ssl  7700  aptiprleml  7706  aptiprlemu  7707  ltmprr  7709  archpr  7710  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemdisj  7718  cauappcvgprlemloc  7719  cauappcvgprlem1  7726  cauappcvgprlem2  7727  cauappcvgprlemlim  7728  caucvgprlemnkj  7733  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlem2  7747  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnjltk  7758  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemdisj  7769  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  caucvgprprlemaddq  7775  caucvgprprlem2  7777  suplocexprlemrl  7784  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  suplocexprlemlub  7791  recexgt0sr  7840  mulgt0sr  7845  prsrriota  7855  caucvgsrlemoffres  7867  suplocsrlem  7875  cnm  7899  addcnsr  7901  mulcnsr  7902  mulcnsrec  7910  axaddcl  7931  axmulcl  7933  axmulcom  7938  rereceu  7956  recriota  7957  axcaucvglemres  7966  axpre-suploclemres  7968  lelttr  8115  ltletr  8116  readdcan  8166  addcan  8206  addcan2  8207  addsub4  8269  ltadd2  8446  le2add  8471  lt2add  8472  lt2sub  8487  le2sub  8488  eqord1  8510  rimul  8612  rereim  8613  ltmul1  8619  apreim  8630  mulreim  8631  apcotr  8634  apadd1  8635  addext  8637  apneg  8638  mulext1  8639  mulext  8641  ltleap  8659  aprcl  8673  mulap0  8681  mulcanapd  8688  receuap  8696  recapb  8698  rec11ap  8737  rec11rap  8738  divdivdivap  8740  ddcanap  8753  divadddivap  8754  conjmulap  8756  subrecap  8866  prodgt0gt0  8878  prodge0  8881  ltmul12a  8887  lemulge11  8893  lt2mul2div  8906  ltrec  8910  lerec  8911  lt2msq  8913  lerec2  8916  le2msq  8928  msq11  8929  ledivp1  8930  mulle0r  8971  suprzclex  9424  peano5uzti  9434  supinfneg  9669  infsupneg  9670  qapne  9713  xrlelttr  9881  xrltletr  9882  xrre  9895  xaddge0  9953  xle2add  9954  xlt2add  9955  divelunit  10077  fzass4  10137  fzocatel  10275  zsupcllemstep  10319  zssinfcl  10322  suprzubdc  10326  zsupssdc  10328  suprzcl2dc  10329  exbtwnzlemex  10339  rebtwn2z  10344  qbtwnre  10346  modqid  10441  modqcyc  10451  modqaddabs  10454  modqaddmod  10455  mulqaddmodid  10456  modqadd2mod  10466  modqltm1p1mod  10468  modqsubmod  10474  modqsubmodmod  10475  modqmulmod  10481  modqmulmodr  10482  modqaddmulmod  10483  modqsubdir  10485  frec2uzisod  10499  iseqovex  10550  seqvalcd  10553  seq1g  10555  seqf  10556  seqovcd  10559  seqm1g  10566  seq3fveq2  10567  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  iseqf1olemnab  10593  seqf1oglem1  10611  seqf1og  10613  seq3id2  10618  seqhomog  10622  seq3distr  10624  expcl2lemap  10643  expnegzap  10665  ltexp2a  10683  le2sq2  10707  nn0ltexp2  10801  nn0opth2  10816  bcval5  10855  hashcl  10873  hashen  10876  fihashdom  10895  hashunlem  10896  hashun  10897  fimaxq  10919  zfz1isolem1  10932  zfz1iso  10933  lencl  10939  sswrd  10944  fstwrdne0  10974  cvg1nlemres  11150  cvg1n  11151  recvguniq  11160  resqrexlemp1rp  11171  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemex  11190  sqrtmul  11200  sqrtsq  11209  absexpzap  11245  absle  11254  abs3lem  11276  amgm2  11283  maxleastlt  11380  maxltsup  11383  fimaxre2  11392  xrmaxleastlt  11421  xrmaxltsup  11423  xrmaxaddlem  11425  climcn2  11474  addcn2  11475  mulcn2  11477  reccn2ap  11478  climcau  11512  summodclem2  11547  summodc  11548  fsumf1o  11555  fisumss  11557  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  fsum2dlemstep  11599  mptfzshft  11607  fsumrev  11608  fsummulc2  11613  modfsummod  11623  fsumrelem  11636  binom  11649  cvgratnn  11696  mertenslemub  11699  prodmodc  11743  zproddc  11744  fprodf1o  11753  fprodssdc  11755  fprodmul  11756  fprodrev  11784  fprod2dlemstep  11787  efcllem  11824  tanaddaplem  11903  dvdsval2  11955  moddvds  11964  dvdsabseq  12012  dvdsflip  12016  oexpneg  12042  fldivndvdslt  12102  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemeu  12174  dfgcd3  12177  bezout  12178  dvdsmulgcd  12192  bezoutr  12199  nninfctlemfo  12207  ialgrlem1st  12210  lcmgcdlem  12245  coprmdvds2  12261  qredeu  12265  rpdvds  12267  isprm5lem  12309  isprm6  12315  pw2dvdslemn  12333  nonsq  12375  crth  12392  eulerthlemh  12399  pclemdc  12457  pcprendvds2  12460  pceu  12464  pcval  12465  pczpre  12466  pcmul  12470  pcqmul  12472  pcqcl  12475  pcid  12493  pcneg  12494  pcgcd1  12497  pc2dvds  12499  pcprmpw2  12502  difsqpwdvds  12507  pcmpt  12512  pockthg  12526  1arith  12536  mul4sq  12563  4sqexercise2  12568  ennnfonelemg  12620  ennnfonelemex  12631  ennnfonelemrnh  12633  ennnfonelemrn  12636  ennnfonelemdm  12637  ennnfonelemnn0  12639  ennnfonelemim  12641  ennnfone  12642  ctinfomlemom  12644  ctinf  12647  ctiunctlemfo  12656  nninfdclemcl  12665  nninfdclemf  12666  nninfdclemp1  12667  unbendc  12671  isstruct2r  12689  setscom  12718  qusval  12966  ercpbl  12974  opifismgmdc  13014  grpinvalem  13028  grprida  13030  igsumvalx  13032  gsumfzval  13034  gsumpropd2  13036  gsumval2  13040  sgrppropd  13056  mndpropd  13081  issubmnd  13083  submnd0  13085  mhmf1o  13102  0mhm  13118  resmhm  13119  mhmco  13122  mhmima  13123  mhmeql  13124  gsumwsubmcl  13128  gsumfzcl  13131  grppropd  13149  grpinvid1  13184  grpinvid2  13185  grplcan  13194  grplmulf1o  13206  grpnpncan0  13228  dfgrp3mlem  13230  grplactcnv  13234  mulgval  13252  mulgfng  13254  mulg1  13259  mulgnnp1  13260  mulgneg  13270  mulgnndir  13281  mulgdirlem  13283  mulgnn0ass  13288  mulgass  13289  subgmulg  13318  issubg4m  13323  subgintm  13328  0nsg  13344  eqgcpbl  13358  ghmmulg  13386  ghmpreima  13396  ghmeql  13397  ghmnsgima  13398  ghmnsgpreima  13399  ghmf1  13403  ghmf1o  13405  conjghm  13406  conjnmzb  13410  qusghm  13412  ablpncan3  13447  invghm  13459  eqgabl  13460  qusecsub  13461  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  imasrng  13512  qusrng  13514  srglmhm  13549  srgrmhm  13550  ringpropd  13594  ringlghm  13617  ringrghm  13618  imasring  13620  qusring2  13622  opprrngbg  13634  dvdsrvald  13649  dvdsrd  13650  dvdsrex  13654  dvdsrtr  13657  unitgrp  13672  unitpropdg  13704  rhmopp  13732  isnzr2  13740  issubrng2  13766  subrngintm  13768  subrgintm  13799  rhmpropd  13810  aprap  13842  lmodprop2d  13904  rmodislmodlem  13906  lssvacl  13921  lssvsubcl  13922  lssvscl  13931  islss3  13935  lsspropdg  13987  rnglidlmcl  14036  2idlcpblrng  14079  crngridl  14086  expghmap  14163  mulgghm2  14164  mulgrhm  14165  znf1o  14207  znleval  14209  znidom  14213  psrval  14220  epttop  14326  topssnei  14398  restbasg  14404  restopnb  14417  cnfval  14430  cnpfval  14431  iscnp4  14454  cnpnei  14455  cnptopco  14458  cncnp  14466  cnrest2  14472  cnptoprest  14475  cnptoprest2  14476  lmss  14482  lmtopcnp  14486  neitx  14504  txcnp  14507  txrest  14512  txdis  14513  txlm  14515  cnmpt21  14527  imasnopn  14535  xmetres2  14615  blvalps  14624  blval  14625  bl2in  14639  blhalf  14644  blssps  14663  blss  14664  blssexps  14665  blssex  14666  ssblex  14667  blin2  14668  metss2lem  14733  bdmetval  14736  bdmopn  14740  metrest  14742  xmetxp  14743  xmetxpbl  14744  xmettx  14746  metcnp3  14747  txmetcnp  14754  addcncntoplem  14797  elcncf2  14810  mulc1cncf  14825  cncfco  14827  cncfmet  14828  mulcncf  14844  dedekindeulemub  14854  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeu  14859  suplociccex  14861  dedekindicclemub  14863  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthdec  14880  ivthreinc  14881  dich0  14888  limcimolemlt  14900  limcimo  14901  cnplimccntop  14906  limccnp2lem  14912  limccnp2cntop  14913  dvfvalap  14917  dvmptfsum  14961  dveflem  14962  plyco  14995  plycn  14998  plyrecj  14999  reeff1olem  15007  reeff1oleme  15008  eflt  15011  sin0pilem2  15018  pilem3  15019  ptolemy  15060  ioocosf1o  15090  cxplt  15152  cxple  15153  cxplt3  15156  apcxp2  15175  rprelogbmul  15191  rprelogbdiv  15193  logbgt0b  15202  logbgcd1irrap  15206  fsumdvdsmul  15227  perfectlem2  15236  lgsdir2lem5  15273  lgsdir  15276  lgsdi  15278  lgsne0  15279  gausslemma2dlem1f1o  15301  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  lgsquad2  15324  2sqlem6  15361  2sqlem10  15366  nnti  15639  pwtrufal  15642  pwf1oexmid  15644  sssneq  15646  qdencn  15671  cvgcmp2n  15677  trilpolemlt1  15685  trirec0  15688  trirec0xor  15689  redc0  15701  reap0  15702  cndcap  15703  nconstwlpolemgt0  15708  neap0mkv  15713  supfz  15715  inffz  15716