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  4726  opabssxpd  4811  0xp  4855  imainss  5203  iotam  5369  fvmptt  5797  fcof1o  5995  isotr  6022  riota5f  6065  ovmpodf  6220  unielxp  6408  fnmpoovd  6451  1stconst  6457  2ndconst  6458  cnvf1olem  6460  fvn0elsupp  6491  suppcofn  6506  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemres  6620  tfrcllemres  6633  tfrcldm  6634  frecabcl  6670  nnaordi  6781  swoer  6835  qliftfun  6891  ecopovsymg  6908  th3qlem1  6911  pw2f1odclem  7134  mapen  7146  mapxpen  7148  fidifsnen  7172  fisbth  7187  findcard2d  7195  findcard2sd  7196  diffisn  7197  diffifi  7198  ac6sfi  7202  fidcen  7203  fimax2gtri  7206  fientri3  7222  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fisseneq  7242  exmidssfi  7246  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  ordiso2  7375  difinfsnlem  7439  difinfinf  7441  ctmlemr  7448  ctssdccl  7451  fodjum  7486  fodju0  7487  omniwomnimkv  7507  exmidfodomrlemrALT  7555  netap  7620  exmidmotap  7627  cc1  7631  cc2lem  7632  cc3  7634  cc4f  7635  cc4n  7637  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  distrnqg  7754  ltexnqq  7775  subhalfnqq  7781  distrnq0  7826  prarloclemup  7862  prarloclem3  7864  prarloc  7870  genplt2i  7877  nqprl  7918  nqpru  7919  prmuloc  7933  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltaddpr  7964  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprlem  7985  ltaprg  7986  prplnqu  7987  addextpr  7988  recexprlemdisj  7997  recexprlemloc  7998  recexprlem1ssl  8000  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  recexgt0sr  8140  mulgt0sr  8145  prsrriota  8155  caucvgsrlemoffres  8167  suplocsrlem  8175  cnm  8199  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axaddcl  8231  axmulcl  8233  axmulcom  8238  rereceu  8256  recriota  8257  axcaucvglemres  8266  axpre-suploclemres  8268  lelttr  8414  ltletr  8415  readdcan  8467  addcan  8507  addcan2  8508  addsub4  8570  ltadd2  8748  le2add  8773  lt2add  8774  lt2sub  8789  le2sub  8790  eqord1  8812  rimul  8915  rereim  8916  ltmul1  8922  apreim  8933  mulreim  8934  apcotr  8937  apadd1  8938  addext  8940  apneg  8941  mulext1  8942  mulext  8944  ltleap  8962  aprcl  8976  mulap0  8984  mulcanapd  8991  receuap  9001  recapb  9003  rec11ap  9042  rec11rap  9043  divdivdivap  9045  ddcanap  9058  divadddivap  9059  conjmulap  9061  subrecap  9171  prodgt0gt0  9183  prodge0  9186  ltmul12a  9192  lemulge11  9198  lt2mul2div  9211  ltrec  9215  lerec  9216  lt2msq  9218  lerec2  9221  le2msq  9233  msq11  9234  ledivp1  9235  mulle0r  9276  suprzclex  9748  peano5uzti  9758  supinfneg  10004  infsupneg  10005  qapne  10048  xrlelttr  10218  xrltletr  10219  xrre  10232  xaddge0  10290  xle2add  10291  xlt2add  10292  divelunit  10414  fzass4  10478  fzocatel  10627  zsupcllemstep  10672  zssinfcl  10675  infssfzcldc  10679  infssfzledc  10680  suprzubdc  10681  zsupssdc  10683  suprzcl2dc  10684  exbtwnzlemex  10694  rebtwn2z  10699  qbtwnre  10701  modqid  10799  modqcyc  10809  modqaddabs  10812  modqaddmod  10813  mulqaddmodid  10814  modqadd2mod  10824  modqltm1p1mod  10826  modqsubmod  10832  modqsubmodmod  10833  modqmulmod  10839  modqmulmodr  10840  modqaddmulmod  10841  modqsubdir  10843  frec2uzisod  10857  iseqovex  10908  seqvalcd  10911  seq1g  10913  seqf  10914  seqovcd  10917  seqm1g  10924  seq3fveq2  10925  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  iseqf1olemnab  10951  seqf1oglem1  10969  seqf1og  10971  seq3id2  10976  seqhomog  10980  seq3distr  10982  expcl2lemap  11001  expnegzap  11023  ltexp2a  11041  le2sq2  11065  nn0ltexp2  11161  nn0opth2  11176  bcval5  11215  hashcl  11234  hashen  11237  fihashdom  11257  hashunlem  11258  hashun  11259  hashmap  11282  fimaxq  11284  hashfibclem  11296  hashfibc  11297  hashf1lem1  11299  hashf1lem2  11300  hashf1  11301  zfz1isolem1  11306  zfz1iso  11307  lencl  11322  sswrd  11327  fstwrdne0  11358  lswlgt0cl  11371  ccatw2s1p1g  11427  ccat2s1fstg  11430  swrdval  11434  wrdind  11508  wrd2ind  11509  swrdccatfn  11510  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  pfxccat3a  11524  reuccatpfxs1  11533  cvg1nlemres  11765  cvg1n  11766  recvguniq  11775  resqrexlemp1rp  11786  resqrexlemoverl  11801  resqrexlemglsq  11802  resqrexlemex  11805  sqrtmul  11815  sqrtsq  11824  absexpzap  11861  absle  11870  abs3lem  11892  amgm2  11899  maxleastlt  11996  maxltsup  11999  fimaxre2  12008  xrmaxleastlt  12038  xrmaxltsup  12040  xrmaxaddlem  12042  climcn2  12091  addcn2  12092  mulcn2  12094  reccn2ap  12095  climcau  12129  summodclem2  12165  summodc  12166  fsumf1o  12173  fisumss  12175  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  fsum2dlemstep  12217  mptfzshft  12225  fsumrev  12226  fsummulc2  12231  modfsummod  12241  fsumrelem  12254  binom  12267  cvgratnn  12314  mertenslemub  12317  prodmodc  12361  zproddc  12362  fprodf1o  12371  fprodssdc  12373  fprodmul  12374  fprodrev  12402  fprod2dlemstep  12405  efcllem  12442  tanaddaplem  12521  dvdsval2  12573  moddvds  12582  dvdsabseq  12630  dvdsflip  12634  oexpneg  12660  fldivndvdslt  12720  bitsfi  12740  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemeu  12800  dfgcd3  12803  bezout  12804  dvdsmulgcd  12818  bezoutr  12825  nninfctlemfo  12833  ialgrlem1st  12836  lcmgcdlem  12871  coprmdvds2  12887  qredeu  12891  rpdvds  12893  isprm5lem  12936  isprm6  12942  pwbdvdslemn  12960  nnmaxpwlemparts  12968  nonsq  13003  crth  13022  eulerthlemh  13029  pclemdc  13087  pcprendvds2  13090  pceu  13094  pcval  13095  pczpre  13096  pcmul  13100  pcqmul  13102  pcqcl  13105  pcid  13123  pcneg  13124  pcgcd1  13127  pc2dvds  13129  pcprmpw2  13132  difsqpwdvds  13137  pcmpt  13142  pockthg  13156  1arith  13166  mul4sq  13193  4sqexercise2  13198  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemg  13343  ennnfonelemex  13354  ennnfonelemrnh  13356  ennnfonelemrn  13359  ennnfonelemdm  13360  ennnfonelemnn0  13362  ennnfonelemim  13364  ennnfone  13365  ctinfomlemom  13367  ctinf  13370  ctiunctlemfo  13379  nninfdclemcl  13388  nninfdclemf  13389  nninfdclemp1  13390  unbendc  13394  isstruct2r  13412  setscom  13441  qusval  13693  ercpbl  13701  opifismgmdc  13740  grpinvalem  13754  grprida  13756  gzsumvalx  13758  gzsumfzval  13760  gzsumval2  13763  sgrppropd  13777  mndpropd  13802  issubmnd  13804  submnd0  13806  mhmf1o  13826  0mhm  13842  resmhm  13843  mhmco  13846  mhmima  13847  mhmeql  13848  gzsumwsubmcl  13850  gzsumcl  13853  grppropd  13871  grpinvid1  13906  grpinvid2  13907  grplcan  13916  grplmulf1o  13928  grpnpncan0  13950  dfgrp3mlem  13952  grplactcnv  13956  mulgval  13974  mulgfng  13976  mulg1  13981  mulgnnp1  13982  mulgneg  13992  mulgnndir  14003  mulgdirlem  14005  mulgnn0ass  14010  mulgass  14011  subgmulg  14040  issubg4m  14045  subgintm  14050  0nsg  14066  eqgcpbl  14080  ghmmulg  14108  ghmpreima  14118  ghmeql  14119  ghmnsgima  14120  ghmnsgpreima  14121  ghmf1  14125  ghmf1o  14127  conjghm  14128  conjnmzb  14132  qusghm  14134  cmnsubm  14161  ablpncan3  14170  invghm  14182  eqgabl  14183  qusecsub  14184  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gsumvalfi  14201  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  prdssgrpd  14240  prdsmndd  14243  pwssub  14265  imasrng  14304  qusrng  14306  srglmhm  14346  srgrmhm  14347  ringpropd  14392  ringlghm  14415  ringrghm  14416  imasring  14418  qusring2  14420  opprrngbg  14432  dvdsrvald  14449  dvdsrd  14450  dvdsrex  14454  dvdsrtr  14457  unitgrp  14472  unitpropdg  14504  rhmopp  14532  isnzr2  14540  issubrng2  14567  subrngintm  14569  subrgintm  14600  rhmpropd  14611  ringunitap  14642  aprap  14647  drngunitap  14657  lmodprop2d  14734  rmodislmodlem  14736  lssvacl  14751  lssvsubcl  14752  lssvscl  14761  islss3  14765  lsspropdg  14817  rnglidlmcl  14866  2idlcpblrng  14909  crngridl  14916  gsumfsum  14972  expghmap  14991  mulgghm2  14992  mulgrhm  14993  znf1o  15035  znleval  15037  znidom  15041  issubassa3  15061  assapropd  15063  asclghm  15074  issubassa2  15084  psrval  15099  psrbagcon  15111  psrbagconf1o  15113  mplsubgfilemcl  15139  epttop  15240  topssnei  15312  restbasg  15318  restopnb  15331  cnfval  15344  cnpfval  15345  iscnp4  15368  cnpnei  15369  cnptopco  15372  cncnp  15380  cnrest2  15386  cnptoprest  15389  cnptoprest2  15390  lmss  15396  lmtopcnp  15400  neitx  15418  txcnp  15421  txrest  15426  txdis  15427  txlm  15429  cnmpt21  15441  imasnopn  15449  xmetres2  15529  blvalps  15538  blval  15539  bl2in  15553  blhalf  15558  blssps  15577  blss  15578  blssexps  15579  blssex  15580  ssblex  15581  blin2  15582  metss2lem  15647  bdmetval  15650  bdmopn  15654  metrest  15656  xmetxp  15657  xmetxpbl  15658  xmettx  15660  metcnp3  15661  txmetcnp  15668  addcncntoplem  15711  elcncf2  15724  mulc1cncf  15739  cncfco  15741  cncfmet  15742  mulcncf  15758  dedekindeulemub  15768  dedekindeulemloc  15769  dedekindeulemlu  15771  dedekindeu  15773  suplociccex  15775  dedekindicclemub  15777  dedekindicclemloc  15778  dedekindicclemlu  15780  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthdec  15794  ivthreinc  15795  dich0  15802  limcimolemlt  15814  limcimo  15815  cnplimccntop  15820  limccnp2lem  15826  limccnp2cntop  15827  dvfvalap  15831  dvmptfsum  15875  dveflem  15876  plyco  15909  plycn  15912  plyrecj  15913  reeff1olem  15921  reeff1oleme  15922  eflt  15925  sin0pilem2  15933  pilem3  15934  ptolemy  15975  ioocosf1o  16005  logdivlt  16046  logdivle  16047  cxplt  16071  cxple  16072  cxplt3  16075  apcxp2  16094  rprelogbmul  16110  rprelogbdiv  16112  logbgt0b  16121  logbgcd1irrap  16125  zprmlogbap  16137  pellexlem3  16150  ppinprm  16171  fsumdvdsmul  16186  perfectlem2  16198  bposlem3  16211  lgsdir2lem5  16249  lgsdir  16252  lgsdi  16254  lgsne0  16255  gausslemma2dlem1f1o  16277  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  lgsquad2  16300  2sqlem6  16337  2sqlem10  16342  upgredg  16483  uhgrissubgr  16600  subgrprop3  16601  upgrspanop  16622  umgrspanop  16623  usgrspanop  16624  vtxedgfi  16628  vtxlpfi  16629  upgr2wlkdc  16716  clwwlkccatlem  16739  eupth2lemsfi  16817  depindlem3  16847  nnti  17120  pwtrufal  17125  pwf1oexmid  17127  sssneq  17130  qdencn  17170  cvgcmp2n  17180  trilpolemlt1  17188  trirec0  17191  trirec0xor  17192  qdiff  17196  redc0  17205  reap0  17206  cndcap  17207  nconstwlpolemgt0  17212  neap0mkv  17217  supfz  17219  inffz  17220