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  3070  disjiun  4013  reg3exmidlemwe  4593  0xp  4721  imainss  5059  iotam  5223  fvmptt  5623  fcof1o  5806  isotr  5833  riota5f  5871  ovmpodf  6023  unielxp  6193  fnmpoovd  6234  1stconst  6240  2ndconst  6241  cnvf1olem  6243  tfrlemi14d  6352  tfrexlem  6353  tfr1onlemres  6368  tfrcllemres  6381  tfrcldm  6382  frecabcl  6418  nnaordi  6527  swoer  6581  qliftfun  6635  ecopovsymg  6652  th3qlem1  6655  mapen  6864  mapxpen  6866  fidifsnen  6888  fisbth  6901  findcard2d  6909  findcard2sd  6910  diffisn  6911  diffifi  6912  ac6sfi  6916  fimax2gtri  6919  fientri3  6932  nnwetri  6933  unsnfi  6936  unsnfidcex  6937  unsnfidcel  6938  fisseneq  6949  fidcenumlemrk  6971  fidcenumlemr  6972  isbth  6984  ordiso2  7052  difinfsnlem  7116  difinfinf  7118  ctmlemr  7125  ctssdccl  7128  fodjum  7162  fodju0  7163  omniwomnimkv  7183  exmidfodomrlemrALT  7220  netap  7271  exmidmotap  7278  cc1  7282  cc2lem  7283  cc3  7285  cc4f  7286  cc4n  7288  dfplpq2  7371  dfmpq2  7372  mulpipqqs  7390  distrnqg  7404  ltexnqq  7425  subhalfnqq  7431  distrnq0  7476  prarloclemup  7512  prarloclem3  7514  prarloc  7520  genplt2i  7527  nqprl  7568  nqpru  7569  prmuloc  7583  mullocpr  7588  distrlem4prl  7601  distrlem4pru  7602  ltaddpr  7614  ltexprlemopl  7618  ltexprlemlol  7619  ltexprlemopu  7620  ltexprlemupu  7621  ltexprlemrl  7627  ltexprlemru  7629  addcanprleml  7631  addcanprlemu  7632  ltaprlem  7635  ltaprg  7636  prplnqu  7637  addextpr  7638  recexprlemdisj  7647  recexprlemloc  7648  recexprlem1ssl  7650  aptiprleml  7656  aptiprlemu  7657  ltmprr  7659  archpr  7660  cauappcvgprlemopl  7663  cauappcvgprlemopu  7665  cauappcvgprlemdisj  7668  cauappcvgprlemloc  7669  cauappcvgprlem1  7676  cauappcvgprlem2  7677  cauappcvgprlemlim  7678  caucvgprlemnkj  7683  caucvgprlemopl  7686  caucvgprlemopu  7688  caucvgprlemdisj  7691  caucvgprlemloc  7692  caucvgprlem2  7697  caucvgprprlemnkltj  7706  caucvgprprlemnkeqj  7707  caucvgprprlemnjltk  7708  caucvgprprlemmu  7712  caucvgprprlemopl  7714  caucvgprprlemopu  7716  caucvgprprlemdisj  7719  caucvgprprlemloc  7720  caucvgprprlemexbt  7723  caucvgprprlemaddq  7725  caucvgprprlem2  7727  suplocexprlemrl  7734  suplocexprlemmu  7735  suplocexprlemru  7736  suplocexprlemdisj  7737  suplocexprlemloc  7738  suplocexprlemex  7739  suplocexprlemub  7740  suplocexprlemlub  7741  recexgt0sr  7790  mulgt0sr  7795  prsrriota  7805  caucvgsrlemoffres  7817  suplocsrlem  7825  cnm  7849  addcnsr  7851  mulcnsr  7852  mulcnsrec  7860  axaddcl  7881  axmulcl  7883  axmulcom  7888  rereceu  7906  recriota  7907  axcaucvglemres  7916  axpre-suploclemres  7918  lelttr  8064  ltletr  8065  readdcan  8115  addcan  8155  addcan2  8156  addsub4  8218  ltadd2  8394  le2add  8419  lt2add  8420  lt2sub  8435  le2sub  8436  eqord1  8458  rimul  8560  rereim  8561  ltmul1  8567  apreim  8578  mulreim  8579  apcotr  8582  apadd1  8583  addext  8585  apneg  8586  mulext1  8587  mulext  8589  ltleap  8607  aprcl  8621  mulap0  8629  mulcanapd  8636  receuap  8644  recapb  8646  rec11ap  8685  rec11rap  8686  divdivdivap  8688  ddcanap  8701  divadddivap  8702  conjmulap  8704  subrecap  8814  prodgt0gt0  8826  prodge0  8829  ltmul12a  8835  lemulge11  8841  lt2mul2div  8854  ltrec  8858  lerec  8859  lt2msq  8861  lerec2  8864  le2msq  8876  msq11  8877  ledivp1  8878  mulle0r  8919  suprzclex  9369  peano5uzti  9379  supinfneg  9613  infsupneg  9614  qapne  9657  xrlelttr  9824  xrltletr  9825  xrre  9838  xaddge0  9896  xle2add  9897  xlt2add  9898  divelunit  10020  fzass4  10080  fzocatel  10217  exbtwnzlemex  10268  rebtwn2z  10273  qbtwnre  10275  modqid  10367  modqcyc  10377  modqaddabs  10380  modqaddmod  10381  mulqaddmodid  10382  modqadd2mod  10392  modqltm1p1mod  10394  modqsubmod  10400  modqsubmodmod  10401  modqmulmod  10407  modqmulmodr  10408  modqaddmulmod  10409  modqsubdir  10411  frec2uzisod  10425  iseqovex  10474  seqvalcd  10477  seqf  10479  seqovcd  10481  seq3fveq2  10487  seq3shft2  10491  monoord  10494  seq3split  10497  iseqf1olemnab  10506  seq3id2  10527  seq3distr  10531  expcl2lemap  10550  expnegzap  10572  ltexp2a  10590  le2sq2  10614  nn0ltexp2  10707  nn0opth2  10722  bcval5  10761  hashcl  10779  hashen  10782  fihashdom  10801  hashunlem  10802  hashun  10803  fimaxq  10825  zfz1isolem1  10838  zfz1iso  10839  cvg1nlemres  11012  cvg1n  11013  recvguniq  11022  resqrexlemp1rp  11033  resqrexlemoverl  11048  resqrexlemglsq  11049  resqrexlemex  11052  sqrtmul  11062  sqrtsq  11071  absexpzap  11107  absle  11116  abs3lem  11138  amgm2  11145  maxleastlt  11242  maxltsup  11245  fimaxre2  11253  xrmaxleastlt  11282  xrmaxltsup  11284  xrmaxaddlem  11286  climcn2  11335  addcn2  11336  mulcn2  11338  reccn2ap  11339  climcau  11373  summodclem2  11408  summodc  11409  fsumf1o  11416  fisumss  11418  fsum3cvg3  11422  fsumcl2lem  11424  fsumadd  11432  fsum2dlemstep  11460  mptfzshft  11468  fsumrev  11469  fsummulc2  11474  modfsummod  11484  fsumrelem  11497  binom  11510  cvgratnn  11557  mertenslemub  11560  prodmodc  11604  zproddc  11605  fprodf1o  11614  fprodssdc  11616  fprodmul  11617  fprodrev  11645  fprod2dlemstep  11648  efcllem  11685  tanaddaplem  11764  dvdsval2  11815  moddvds  11824  dvdsabseq  11871  dvdsflip  11875  oexpneg  11900  fldivndvdslt  11958  zsupcllemstep  11964  zssinfcl  11967  suprzubdc  11971  zsupssdc  11973  suprzcl2dc  11974  bezoutlemnewy  12015  bezoutlemstep  12016  bezoutlemeu  12026  dfgcd3  12029  bezout  12030  dvdsmulgcd  12044  bezoutr  12051  ialgrlem1st  12060  lcmgcdlem  12095  coprmdvds2  12111  qredeu  12115  rpdvds  12117  isprm5lem  12159  isprm6  12165  pw2dvdslemn  12183  nonsq  12225  crth  12242  eulerthlemh  12249  pclemdc  12306  pcprendvds2  12309  pceu  12313  pcval  12314  pczpre  12315  pcmul  12319  pcqmul  12321  pcqcl  12324  pcid  12341  pcneg  12342  pcgcd1  12345  pc2dvds  12347  pcprmpw2  12350  difsqpwdvds  12355  pcmpt  12359  pockthg  12373  1arith  12383  mul4sq  12410  ennnfonelemg  12422  ennnfonelemex  12433  ennnfonelemrnh  12435  ennnfonelemrn  12438  ennnfonelemdm  12439  ennnfonelemnn0  12441  ennnfonelemim  12443  ennnfone  12444  ctinfomlemom  12446  ctinf  12449  ctiunctlemfo  12458  nninfdclemcl  12467  nninfdclemf  12468  nninfdclemp1  12469  unbendc  12473  isstruct2r  12491  setscom  12520  qusval  12766  ercpbl  12773  opifismgmdc  12813  grpinvalem  12827  grprida  12829  sgrppropd  12842  mndpropd  12867  issubmnd  12869  submnd0  12871  mhmf1o  12888  0mhm  12904  resmhm  12905  mhmco  12908  mhmima  12909  mhmeql  12910  grppropd  12928  grpinvid1  12962  grpinvid2  12963  grplcan  12972  grplmulf1o  12984  grpnpncan0  13006  dfgrp3mlem  13008  grplactcnv  13012  mulgval  13030  mulgfng  13032  mulg1  13035  mulgnnp1  13036  mulgneg  13046  mulgnndir  13057  mulgdirlem  13059  mulgnn0ass  13064  mulgass  13065  subgmulg  13093  issubg4m  13098  subgintm  13103  0nsg  13119  eqgcpbl  13133  ghmmulg  13156  ghmpreima  13166  ghmeql  13167  ghmnsgima  13168  ghmnsgpreima  13169  ghmf1  13173  ghmf1o  13175  conjghm  13176  conjnmzb  13180  qusghm  13182  ablpncan3  13217  eqgabl  13228  qusecsub  13229  imasrng  13271  qusrng  13273  srglmhm  13308  srgrmhm  13309  ringpropd  13353  imasring  13375  qusring2  13377  opprrngbg  13389  dvdsrvald  13404  dvdsrd  13405  dvdsrex  13409  dvdsrtr  13412  unitgrp  13427  unitpropdg  13459  rhmopp  13487  issubrng2  13518  subrngintm  13520  subrgintm  13551  aprap  13563  lmodprop2d  13625  rmodislmodlem  13627  lssvacl  13642  lssvsubcl  13643  lssvscl  13652  islss3  13656  lsspropdg  13708  rnglidlmcl  13757  2idlcpblrng  13799  crngridl  13805  mulgghm2  13867  mulgrhm  13868  epttop  13987  topssnei  14059  restbasg  14065  restopnb  14078  cnfval  14091  cnpfval  14092  iscnp4  14115  cnpnei  14116  cnptopco  14119  cncnp  14127  cnrest2  14133  cnptoprest  14136  cnptoprest2  14137  lmss  14143  lmtopcnp  14147  neitx  14165  txcnp  14168  txrest  14173  txdis  14174  txlm  14176  cnmpt21  14188  imasnopn  14196  xmetres2  14276  blvalps  14285  blval  14286  bl2in  14300  blhalf  14305  blssps  14324  blss  14325  blssexps  14326  blssex  14327  ssblex  14328  blin2  14329  metss2lem  14394  bdmetval  14397  bdmopn  14401  metrest  14403  xmetxp  14404  xmetxpbl  14405  xmettx  14407  metcnp3  14408  txmetcnp  14415  addcncntoplem  14448  elcncf2  14458  mulc1cncf  14473  cncfco  14475  cncfmet  14476  mulcncf  14488  dedekindeulemub  14493  dedekindeulemloc  14494  dedekindeulemlu  14496  dedekindeu  14498  suplociccex  14500  dedekindicclemub  14502  dedekindicclemloc  14503  dedekindicclemlu  14505  dedekindicc  14508  ivthinclemlopn  14511  ivthinclemuopn  14513  ivthdec  14519  limcimolemlt  14530  limcimo  14531  cnplimccntop  14536  limccnp2lem  14542  limccnp2cntop  14543  dvfvalap  14547  dveflem  14584  reeff1olem  14589  reeff1oleme  14590  eflt  14593  sin0pilem2  14600  pilem3  14601  ptolemy  14642  ioocosf1o  14672  cxplt  14733  cxple  14734  cxplt3  14737  apcxp2  14755  rprelogbmul  14770  rprelogbdiv  14772  logbgt0b  14781  logbgcd1irrap  14785  lgsdir2lem5  14830  lgsdir  14833  lgsdi  14835  lgsne0  14836  lgseisenlem2  14848  2sqlem6  14864  2sqlem10  14869  nnti  15142  pwtrufal  15145  pwf1oexmid  15147  sssneq  15149  qdencn  15173  cvgcmp2n  15179  trilpolemlt1  15187  trirec0  15190  trirec0xor  15191  redc0  15203  reap0  15204  cndcap  15205  nconstwlpolemgt0  15210  neap0mkv  15215  supfz  15217  inffz  15218