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  7376  difinfsnlem  7440  difinfinf  7442  ctmlemr  7449  ctssdccl  7452  fodjum  7487  fodju0  7488  omniwomnimkv  7508  exmidfodomrlemrALT  7556  netap  7621  exmidmotap  7628  cc1  7632  cc2lem  7633  cc3  7635  cc4f  7636  cc4n  7638  dfplpq2  7722  dfmpq2  7723  mulpipqqs  7741  distrnqg  7755  ltexnqq  7776  subhalfnqq  7782  distrnq0  7827  prarloclemup  7863  prarloclem3  7865  prarloc  7871  genplt2i  7878  nqprl  7919  nqpru  7920  prmuloc  7934  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltaddpr  7965  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltaprlem  7986  ltaprg  7987  prplnqu  7988  addextpr  7989  recexprlemdisj  7998  recexprlemloc  7999  recexprlem1ssl  8001  aptiprleml  8007  aptiprlemu  8008  ltmprr  8010  archpr  8011  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlem1  8027  cauappcvgprlem2  8028  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlem2  8048  caucvgprprlemnkltj  8057  caucvgprprlemnkeqj  8058  caucvgprprlemnjltk  8059  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemdisj  8070  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlem2  8078  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  suplocexprlemlub  8092  recexgt0sr  8141  mulgt0sr  8146  prsrriota  8156  caucvgsrlemoffres  8168  suplocsrlem  8176  cnm  8200  addcnsr  8202  mulcnsr  8203  mulcnsrec  8211  axaddcl  8232  axmulcl  8234  axmulcom  8239  rereceu  8257  recriota  8258  axcaucvglemres  8267  axpre-suploclemres  8269  lelttr  8415  ltletr  8416  readdcan  8468  addcan  8508  addcan2  8509  addsub4  8571  ltadd2  8749  le2add  8774  lt2add  8775  lt2sub  8790  le2sub  8791  eqord1  8813  rimul  8916  rereim  8917  ltmul1  8923  apreim  8934  mulreim  8935  apcotr  8938  apadd1  8939  addext  8941  apneg  8942  mulext1  8943  mulext  8945  ltleap  8963  aprcl  8977  mulap0  8985  mulcanapd  8992  receuap  9002  recapb  9004  rec11ap  9043  rec11rap  9044  divdivdivap  9046  ddcanap  9059  divadddivap  9060  conjmulap  9062  subrecap  9172  prodgt0gt0  9184  prodge0  9187  ltmul12a  9193  lemulge11  9199  lt2mul2div  9212  ltrec  9216  lerec  9217  lt2msq  9219  lerec2  9222  le2msq  9234  msq11  9235  ledivp1  9236  mulle0r  9277  suprzclex  9749  peano5uzti  9759  supinfneg  10005  infsupneg  10006  qapne  10049  xrlelttr  10219  xrltletr  10220  xrre  10233  xaddge0  10291  xle2add  10292  xlt2add  10293  divelunit  10415  fzass4  10479  fzocatel  10628  zsupcllemstep  10673  zssinfcl  10676  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  zsupssdc  10684  suprzcl2dc  10685  exbtwnzlemex  10695  rebtwn2z  10700  qbtwnre  10702  modqid  10801  modqcyc  10811  modqaddabs  10814  modqaddmod  10815  mulqaddmodid  10816  modqadd2mod  10826  modqltm1p1mod  10828  modqsubmod  10834  modqsubmodmod  10835  modqmulmod  10841  modqmulmodr  10842  modqaddmulmod  10843  modqsubdir  10845  frec2uzisod  10859  iseqovex  10910  seqvalcd  10913  seq1g  10915  seqf  10916  seqovcd  10919  seqm1g  10926  seq3fveq2  10927  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  iseqf1olemnab  10953  seqf1oglem1  10971  seqf1og  10973  seq3id2  10978  seqhomog  10982  seq3distr  10984  expcl2lemap  11003  expnegzap  11025  ltexp2a  11043  le2sq2  11067  nn0ltexp2  11163  nn0opth2  11178  bcval5  11217  hashcl  11236  hashen  11239  fihashdom  11259  hashunlem  11260  hashun  11261  hashmap  11284  fimaxq  11286  hashfibclem  11298  hashfibc  11299  hashf1lem1  11301  hashf1lem2  11302  hashf1  11303  zfz1isolem1  11308  zfz1iso  11309  lencl  11324  sswrd  11329  fstwrdne0  11360  lswlgt0cl  11373  ccatw2s1p1g  11429  ccat2s1fstg  11432  swrdval  11436  wrdind  11510  wrd2ind  11511  swrdccatfn  11512  swrdccatin1  11513  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12  11521  pfxccat3a  11526  reuccatpfxs1  11535  cvg1nlemres  11767  cvg1n  11768  recvguniq  11777  resqrexlemp1rp  11788  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemex  11807  sqrtmul  11817  sqrtsq  11826  absexpzap  11863  absle  11872  abs3lem  11894  amgm2  11901  maxleastlt  11998  maxltsup  12001  fimaxre2  12010  fiidxsupcl  12012  xrmaxleastlt  12041  xrmaxltsup  12043  xrmaxaddlem  12045  climcn2  12094  addcn2  12095  mulcn2  12097  reccn2ap  12098  climcau  12132  summodclem2  12168  summodc  12169  fsumf1o  12176  fisumss  12178  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  fsum2dlemstep  12220  mptfzshft  12228  fsumrev  12229  fsummulc2  12234  modfsummod  12244  fsumrelem  12257  binom  12270  cvgratnn  12317  mertenslemub  12320  prodmodc  12364  zproddc  12365  fprodf1o  12374  fprodssdc  12376  fprodmul  12377  fprodrev  12405  fprod2dlemstep  12408  efcllem  12445  tanaddaplem  12524  dvdsval2  12576  moddvds  12585  dvdsabseq  12633  dvdsflip  12637  oexpneg  12663  fldivndvdslt  12723  bitsfi  12743  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemeu  12803  dfgcd3  12806  bezout  12807  dvdsmulgcd  12821  bezoutr  12828  nninfctlemfo  12836  ialgrlem1st  12839  lcmgcdlem  12874  coprmdvds2  12890  qredeu  12894  rpdvds  12896  isprm5lem  12939  isprm6  12945  pwbdvdslemn  12963  nnmaxpwlemparts  12971  nonsq  13006  crth  13025  eulerthlemh  13032  pclemdc  13090  pcprendvds2  13093  pceu  13097  pcval  13098  pczpre  13099  pcmul  13103  pcqmul  13105  pcqcl  13108  pcid  13126  pcneg  13127  pcgcd1  13130  pc2dvds  13132  pcprmpw2  13135  difsqpwdvds  13140  pcmpt  13145  pockthg  13159  1arith  13169  mul4sq  13196  4sqexercise2  13201  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemg  13346  ennnfonelemex  13357  ennnfonelemrnh  13359  ennnfonelemrn  13362  ennnfonelemdm  13363  ennnfonelemnn0  13365  ennnfonelemim  13367  ennnfone  13368  ctinfomlemom  13370  ctinf  13373  ctiunctlemfo  13382  nninfdclemcl  13391  nninfdclemf  13392  nninfdclemp1  13393  unbendc  13397  isstruct2r  13415  setscom  13444  qusval  13697  ercpbl  13705  opifismgmdc  13744  grpinvalem  13758  grprida  13760  gzsumvalx  13762  gzsumfzval  13764  gzsumval2  13767  sgrppropd  13781  mndpropd  13806  issubmnd  13808  submnd0  13810  mhmf1o  13830  0mhm  13846  resmhm  13847  mhmco  13850  mhmima  13851  mhmeql  13852  gzsumwsubmcl  13854  gzsumcl  13857  grppropd  13875  grpinvid1  13910  grpinvid2  13911  grplcan  13920  grplmulf1o  13932  grpnpncan0  13954  dfgrp3mlem  13956  grplactcnv  13960  mulgval  13978  mulgfng  13980  mulg1  13985  mulgnnp1  13986  mulgneg  13996  mulgnndir  14007  mulgdirlem  14009  mulgnn0ass  14014  mulgass  14015  subgmulg  14044  issubg4m  14049  subgintm  14054  0nsg  14070  eqgcpbl  14084  ghmmulg  14112  ghmpreima  14122  ghmeql  14123  ghmnsgima  14124  ghmnsgpreima  14125  ghmf1  14129  ghmf1o  14131  conjghm  14132  conjnmzb  14136  qusghm  14138  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cntrsubgnsg  14169  cmnsubm  14196  ablpncan3  14205  invghm  14217  eqgabl  14218  qusecsub  14219  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gsumvalfi  14236  gsumclfi  14243  gsummptfidmadd  14245  gsumsubmclfi  14247  gsummptfidmsplit  14248  gsumresfi  14254  prdssgrpd  14282  prdsmndd  14285  pwssub  14307  imasrng  14346  qusrng  14348  srglmhm  14388  srgrmhm  14389  ringpropd  14434  ringlghm  14457  ringrghm  14458  imasring  14460  qusring2  14462  opprrngbg  14474  dvdsrvald  14491  dvdsrd  14492  dvdsrex  14496  dvdsrtr  14499  unitgrp  14514  unitpropdg  14546  rhmopp  14574  isnzr2  14582  issubrng2  14609  subrngintm  14611  subrgintm  14642  rhmpropd  14653  ringunitap  14684  aprap  14689  drngunitap  14699  lmodprop2d  14776  rmodislmodlem  14778  lssvacl  14793  lssvsubcl  14794  lssvscl  14803  islss3  14807  lsspropdg  14859  rnglidlmcl  14908  2idlcpblrng  14951  crngridl  14958  gsumfsum  15014  expghmap  15033  mulgghm2  15034  mulgrhm  15035  znf1o  15077  znleval  15079  znidom  15083  issubassa3  15103  assapropd  15105  asclghm  15116  issubassa2  15126  psrval  15141  psrbagcon  15153  psrbaglefifi  15154  psrbagconf1o  15156  mplsubgfilemcl  15189  epttop  15290  topssnei  15362  restbasg  15368  restopnb  15381  cnfval  15394  cnpfval  15395  iscnp4  15418  cnpnei  15419  cnptopco  15422  cncnp  15430  cnrest2  15436  cnptoprest  15439  cnptoprest2  15440  lmss  15446  lmtopcnp  15450  neitx  15468  txcnp  15471  txrest  15476  txdis  15477  txlm  15479  cnmpt21  15491  imasnopn  15499  xmetres2  15579  blvalps  15588  blval  15589  bl2in  15603  blhalf  15608  blssps  15627  blss  15628  blssexps  15629  blssex  15630  ssblex  15631  blin2  15632  metss2lem  15697  bdmetval  15700  bdmopn  15704  metrest  15706  xmetxp  15707  xmetxpbl  15708  xmettx  15710  metcnp3  15711  txmetcnp  15718  addcncntoplem  15761  elcncf2  15774  mulc1cncf  15789  cncfco  15791  cncfmet  15792  mulcncf  15808  dedekindeulemub  15818  dedekindeulemloc  15819  dedekindeulemlu  15821  dedekindeu  15823  suplociccex  15825  dedekindicclemub  15827  dedekindicclemloc  15828  dedekindicclemlu  15830  dedekindicc  15833  ivthinclemlopn  15836  ivthinclemuopn  15838  ivthdec  15844  ivthreinc  15845  dich0  15852  limcimolemlt  15864  limcimo  15865  cnplimccntop  15870  limccnp2lem  15876  limccnp2cntop  15877  dvfvalap  15881  dvmptfsum  15925  dveflem  15926  plyco  15959  plycn  15962  plyrecj  15963  reeff1olem  15971  reeff1oleme  15972  eflt  15975  sin0pilem2  15983  pilem3  15984  ptolemy  16025  ioocosf1o  16056  logdivlt  16098  logdivle  16099  rpcxpmul2z  16122  cxplt  16125  cxple  16126  cxplt3  16129  apcxp2  16148  rprelogbmul  16165  rprelogbdiv  16167  logbgt0b  16176  logbgcd1irrap  16180  zprmlogbap  16192  pellexlem3  16205  efnnfsumcl  16213  ppinprm  16234  chtnprm  16236  efchtqdvds  16239  fsumdvdsmul  16259  chtublem  16269  perfectlem2  16274  bposlem3  16287  lgsdir2lem5  16330  lgsdir  16333  lgsdi  16335  lgsne0  16336  gausslemma2dlem1f1o  16358  lgseisenlem2  16369  lgsquadlem1  16375  lgsquadlem2  16376  lgsquad2lem2  16380  lgsquad2  16381  2sqlem6  16418  2sqlem10  16423  upgredg  16564  uhgrissubgr  16681  subgrprop3  16682  upgrspanop  16703  umgrspanop  16704  usgrspanop  16705  vtxedgfi  16709  vtxlpfi  16710  upgr2wlkdc  16797  clwwlkccatlem  16820  eupth2lemsfi  16898  depindlem3  16928  nnti  17201  pwtrufal  17206  pwf1oexmid  17208  sssneq  17211  qdencn  17251  cvgcmp2n  17261  trilpolemlt1  17270  trirec0  17273  trirec0xor  17274  qdiff  17278  redc0  17287  reap0  17288  cndcap  17289  nconstwlpolemgt0  17294  neap0mkv  17299  supfz  17301  inffz  17302