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 )

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:  dfifp2dc  994  simp1rl  1093  simp2rl  1097  simp3rl  1101  rmob  3145  elpr2elpr  3896  disjiun  4120  reg3exmidlemwe  4721  opabssxpd  4806  0xp  4850  imainss  5198  iotam  5364  fvmptt  5791  fcof1o  5985  isotr  6012  riota5f  6055  ovmpodf  6210  unielxp  6398  fnmpoovd  6441  1stconst  6447  2ndconst  6448  cnvf1olem  6450  fvn0elsupp  6481  suppcofn  6496  tfrlemi14d  6594  tfrexlem  6595  tfr1onlemres  6610  tfrcllemres  6623  tfrcldm  6624  frecabcl  6660  nnaordi  6771  swoer  6825  qliftfun  6881  ecopovsymg  6898  th3qlem1  6901  pw2f1odclem  7124  mapen  7136  mapxpen  7138  fidifsnen  7162  fisbth  7177  findcard2d  7185  findcard2sd  7186  diffisn  7187  diffifi  7188  ac6sfi  7192  fidcen  7193  fimax2gtri  7196  fientri3  7212  nnwetri  7213  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  fisseneq  7232  exmidssfi  7236  fidcenumlemrk  7261  fidcenumlemr  7262  isbth  7274  ordiso2  7365  difinfsnlem  7429  difinfinf  7431  ctmlemr  7438  ctssdccl  7441  fodjum  7476  fodju0  7477  omniwomnimkv  7497  exmidfodomrlemrALT  7545  netap  7610  exmidmotap  7617  cc1  7621  cc2lem  7622  cc3  7624  cc4f  7625  cc4n  7627  dfplpq2  7711  dfmpq2  7712  mulpipqqs  7730  distrnqg  7744  ltexnqq  7765  subhalfnqq  7771  distrnq0  7816  prarloclemup  7852  prarloclem3  7854  prarloc  7860  genplt2i  7867  nqprl  7908  nqpru  7909  prmuloc  7923  mullocpr  7928  distrlem4prl  7941  distrlem4pru  7942  ltaddpr  7954  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  ltaprlem  7975  ltaprg  7976  prplnqu  7977  addextpr  7978  recexprlemdisj  7987  recexprlemloc  7988  recexprlem1ssl  7990  aptiprleml  7996  aptiprlemu  7997  ltmprr  7999  archpr  8000  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlem1  8016  cauappcvgprlem2  8017  cauappcvgprlemlim  8018  caucvgprlemnkj  8023  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlem2  8037  caucvgprprlemnkltj  8046  caucvgprprlemnkeqj  8047  caucvgprprlemnjltk  8048  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemopu  8056  caucvgprprlemdisj  8059  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlemaddq  8065  caucvgprprlem2  8067  suplocexprlemrl  8074  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemex  8079  suplocexprlemub  8080  suplocexprlemlub  8081  recexgt0sr  8130  mulgt0sr  8135  prsrriota  8145  caucvgsrlemoffres  8157  suplocsrlem  8165  cnm  8189  addcnsr  8191  mulcnsr  8192  mulcnsrec  8200  axaddcl  8221  axmulcl  8223  axmulcom  8228  rereceu  8246  recriota  8247  axcaucvglemres  8256  axpre-suploclemres  8258  lelttr  8404  ltletr  8405  readdcan  8456  addcan  8496  addcan2  8497  addsub4  8559  ltadd2  8737  le2add  8762  lt2add  8763  lt2sub  8778  le2sub  8779  eqord1  8801  rimul  8903  rereim  8904  ltmul1  8910  apreim  8921  mulreim  8922  apcotr  8925  apadd1  8926  addext  8928  apneg  8929  mulext1  8930  mulext  8932  ltleap  8950  aprcl  8964  mulap0  8972  mulcanapd  8979  receuap  8989  recapb  8991  rec11ap  9030  rec11rap  9031  divdivdivap  9033  ddcanap  9046  divadddivap  9047  conjmulap  9049  subrecap  9159  prodgt0gt0  9171  prodge0  9174  ltmul12a  9180  lemulge11  9186  lt2mul2div  9199  ltrec  9203  lerec  9204  lt2msq  9206  lerec2  9209  le2msq  9221  msq11  9222  ledivp1  9223  mulle0r  9264  suprzclex  9723  peano5uzti  9733  supinfneg  9974  infsupneg  9975  qapne  10018  xrlelttr  10187  xrltletr  10188  xrre  10201  xaddge0  10259  xle2add  10260  xlt2add  10261  divelunit  10383  fzass4  10446  fzocatel  10595  zsupcllemstep  10640  zssinfcl  10643  infssfzcldc  10647  infssfzledc  10648  suprzubdc  10649  zsupssdc  10651  suprzcl2dc  10652  exbtwnzlemex  10662  rebtwn2z  10667  qbtwnre  10669  modqid  10764  modqcyc  10774  modqaddabs  10777  modqaddmod  10778  mulqaddmodid  10779  modqadd2mod  10789  modqltm1p1mod  10791  modqsubmod  10797  modqsubmodmod  10798  modqmulmod  10804  modqmulmodr  10805  modqaddmulmod  10806  modqsubdir  10808  frec2uzisod  10822  iseqovex  10873  seqvalcd  10876  seq1g  10878  seqf  10879  seqovcd  10882  seqm1g  10889  seq3fveq2  10890  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  iseqf1olemnab  10916  seqf1oglem1  10934  seqf1og  10936  seq3id2  10941  seqhomog  10945  seq3distr  10947  expcl2lemap  10966  expnegzap  10988  ltexp2a  11006  le2sq2  11030  nn0ltexp2  11125  nn0opth2  11140  bcval5  11179  hashcl  11198  hashen  11201  fihashdom  11221  hashunlem  11222  hashun  11223  hashmap  11246  fimaxq  11248  hashfibclem  11260  hashfibc  11261  hashf1lem1  11263  hashf1lem2  11264  hashf1  11265  zfz1isolem1  11270  zfz1iso  11271  lencl  11286  sswrd  11291  fstwrdne0  11322  lswlgt0cl  11335  ccatw2s1p1g  11391  ccat2s1fstg  11394  swrdval  11398  wrdind  11472  wrd2ind  11473  swrdccatfn  11474  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  pfxccat3a  11488  reuccatpfxs1  11497  cvg1nlemres  11729  cvg1n  11730  recvguniq  11739  resqrexlemp1rp  11750  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemex  11769  sqrtmul  11779  sqrtsq  11788  absexpzap  11824  absle  11833  abs3lem  11855  amgm2  11862  maxleastlt  11959  maxltsup  11962  fimaxre2  11971  xrmaxleastlt  12000  xrmaxltsup  12002  xrmaxaddlem  12004  climcn2  12053  addcn2  12054  mulcn2  12056  reccn2ap  12057  climcau  12091  summodclem2  12127  summodc  12128  fsumf1o  12135  fisumss  12137  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  fsum2dlemstep  12179  mptfzshft  12187  fsumrev  12188  fsummulc2  12193  modfsummod  12203  fsumrelem  12216  binom  12229  cvgratnn  12276  mertenslemub  12279  prodmodc  12323  zproddc  12324  fprodf1o  12333  fprodssdc  12335  fprodmul  12336  fprodrev  12364  fprod2dlemstep  12367  efcllem  12404  tanaddaplem  12483  dvdsval2  12535  moddvds  12544  dvdsabseq  12592  dvdsflip  12596  oexpneg  12622  fldivndvdslt  12682  bitsfi  12702  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemeu  12762  dfgcd3  12765  bezout  12766  dvdsmulgcd  12780  bezoutr  12787  nninfctlemfo  12795  ialgrlem1st  12798  lcmgcdlem  12833  coprmdvds2  12849  qredeu  12853  rpdvds  12855  isprm5lem  12897  isprm6  12903  pw2dvdslemn  12921  nonsq  12963  crth  12980  eulerthlemh  12987  pclemdc  13045  pcprendvds2  13048  pceu  13052  pcval  13053  pczpre  13054  pcmul  13058  pcqmul  13060  pcqcl  13063  pcid  13081  pcneg  13082  pcgcd1  13085  pc2dvds  13087  pcprmpw2  13090  difsqpwdvds  13095  pcmpt  13100  pockthg  13114  1arith  13124  mul4sq  13151  4sqexercise2  13156  ballotfilemfc0  13210  ballotfilemfcc  13211  ennnfonelemg  13272  ennnfonelemex  13283  ennnfonelemrnh  13285  ennnfonelemrn  13288  ennnfonelemdm  13289  ennnfonelemnn0  13291  ennnfonelemim  13293  ennnfone  13294  ctinfomlemom  13296  ctinf  13299  ctiunctlemfo  13308  nninfdclemcl  13317  nninfdclemf  13318  nninfdclemp1  13319  unbendc  13323  isstruct2r  13341  setscom  13370  qusval  13621  ercpbl  13629  opifismgmdc  13668  grpinvalem  13682  grprida  13684  gzsumvalx  13686  gzsumfzval  13688  gzsumval2  13691  sgrppropd  13705  mndpropd  13730  issubmnd  13732  submnd0  13734  mhmf1o  13754  0mhm  13770  resmhm  13771  mhmco  13774  mhmima  13775  mhmeql  13776  gzsumwsubmcl  13778  gzsumcl  13781  grppropd  13799  grpinvid1  13834  grpinvid2  13835  grplcan  13844  grplmulf1o  13856  grpnpncan0  13878  dfgrp3mlem  13880  grplactcnv  13884  mulgval  13902  mulgfng  13904  mulg1  13909  mulgnnp1  13910  mulgneg  13920  mulgnndir  13931  mulgdirlem  13933  mulgnn0ass  13938  mulgass  13939  subgmulg  13968  issubg4m  13973  subgintm  13978  0nsg  13994  eqgcpbl  14008  ghmmulg  14036  ghmpreima  14046  ghmeql  14047  ghmnsgima  14048  ghmnsgpreima  14049  ghmf1  14053  ghmf1o  14055  conjghm  14056  conjnmzb  14060  qusghm  14062  cmnsubm  14089  ablpncan3  14098  invghm  14110  eqgabl  14111  qusecsub  14112  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gsumvalfi  14129  gsumclfi  14136  gsummptfidmadd  14138  gsumsubmclfi  14140  prdssgrpd  14168  prdsmndd  14171  pwssub  14193  imasrng  14230  qusrng  14232  srglmhm  14271  srgrmhm  14272  ringpropd  14316  ringlghm  14339  ringrghm  14340  imasring  14342  qusring2  14344  opprrngbg  14356  dvdsrvald  14373  dvdsrd  14374  dvdsrex  14378  dvdsrtr  14381  unitgrp  14396  unitpropdg  14428  rhmopp  14456  isnzr2  14464  issubrng2  14491  subrngintm  14493  subrgintm  14524  rhmpropd  14535  ringunitap  14566  aprap  14571  drngunitap  14581  lmodprop2d  14657  rmodislmodlem  14659  lssvacl  14674  lssvsubcl  14675  lssvscl  14684  islss3  14688  lsspropdg  14740  rnglidlmcl  14789  2idlcpblrng  14832  crngridl  14839  gsumfsum  14895  expghmap  14914  mulgghm2  14915  mulgrhm  14916  znf1o  14958  znleval  14960  znidom  14964  psrval  14973  psrbagcon  14985  psrbagconf1o  14987  mplsubgfilemcl  15013  epttop  15114  topssnei  15186  restbasg  15192  restopnb  15205  cnfval  15218  cnpfval  15219  iscnp4  15242  cnpnei  15243  cnptopco  15246  cncnp  15254  cnrest2  15260  cnptoprest  15263  cnptoprest2  15264  lmss  15270  lmtopcnp  15274  neitx  15292  txcnp  15295  txrest  15300  txdis  15301  txlm  15303  cnmpt21  15315  imasnopn  15323  xmetres2  15403  blvalps  15412  blval  15413  bl2in  15427  blhalf  15432  blssps  15451  blss  15452  blssexps  15453  blssex  15454  ssblex  15455  blin2  15456  metss2lem  15521  bdmetval  15524  bdmopn  15528  metrest  15530  xmetxp  15531  xmetxpbl  15532  xmettx  15534  metcnp3  15535  txmetcnp  15542  addcncntoplem  15585  elcncf2  15598  mulc1cncf  15613  cncfco  15615  cncfmet  15616  mulcncf  15632  dedekindeulemub  15642  dedekindeulemloc  15643  dedekindeulemlu  15645  dedekindeu  15647  suplociccex  15649  dedekindicclemub  15651  dedekindicclemloc  15652  dedekindicclemlu  15654  dedekindicc  15657  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthdec  15668  ivthreinc  15669  dich0  15676  limcimolemlt  15688  limcimo  15689  cnplimccntop  15694  limccnp2lem  15700  limccnp2cntop  15701  dvfvalap  15705  dvmptfsum  15749  dveflem  15750  plyco  15783  plycn  15786  plyrecj  15787  reeff1olem  15795  reeff1oleme  15796  eflt  15799  sin0pilem2  15806  pilem3  15807  ptolemy  15848  ioocosf1o  15878  cxplt  15941  cxple  15942  cxplt3  15945  apcxp2  15964  rprelogbmul  15980  rprelogbdiv  15982  logbgt0b  15991  logbgcd1irrap  15995  pellexlem3  16007  fsumdvdsmul  16019  perfectlem2  16028  lgsdir2lem5  16065  lgsdir  16068  lgsdi  16070  lgsne0  16071  gausslemma2dlem1f1o  16093  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem2  16115  lgsquad2  16116  2sqlem6  16153  2sqlem10  16158  upgredg  16299  uhgrissubgr  16416  subgrprop3  16417  upgrspanop  16438  umgrspanop  16439  usgrspanop  16440  vtxedgfi  16444  vtxlpfi  16445  upgr2wlkdc  16532  clwwlkccatlem  16555  eupth2lemsfi  16633  depindlem3  16663  nnti  16936  pwtrufal  16941  pwf1oexmid  16943  sssneq  16946  qdencn  16977  cvgcmp2n  16987  trilpolemlt1  16995  trirec0  16998  trirec0xor  16999  qdiff  17003  redc0  17012  reap0  17013  cndcap  17014  nconstwlpolemgt0  17019  neap0mkv  17024  supfz  17026  inffz  17027