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  prdssgrpd  14275  prdsmndd  14278  pwssub  14300  imasrng  14339  qusrng  14341  srglmhm  14381  srgrmhm  14382  ringpropd  14427  ringlghm  14450  ringrghm  14451  imasring  14453  qusring2  14455  opprrngbg  14467  dvdsrvald  14484  dvdsrd  14485  dvdsrex  14489  dvdsrtr  14492  unitgrp  14507  unitpropdg  14539  rhmopp  14567  isnzr2  14575  issubrng2  14602  subrngintm  14604  subrgintm  14635  rhmpropd  14646  ringunitap  14677  aprap  14682  drngunitap  14692  lmodprop2d  14769  rmodislmodlem  14771  lssvacl  14786  lssvsubcl  14787  lssvscl  14796  islss3  14800  lsspropdg  14852  rnglidlmcl  14901  2idlcpblrng  14944  crngridl  14951  gsumfsum  15007  expghmap  15026  mulgghm2  15027  mulgrhm  15028  znf1o  15070  znleval  15072  znidom  15076  issubassa3  15096  assapropd  15098  asclghm  15109  issubassa2  15119  psrval  15134  psrbagcon  15146  psrbaglefifi  15147  psrbagconf1o  15149  mplsubgfilemcl  15181  epttop  15282  topssnei  15354  restbasg  15360  restopnb  15373  cnfval  15386  cnpfval  15387  iscnp4  15410  cnpnei  15411  cnptopco  15414  cncnp  15422  cnrest2  15428  cnptoprest  15431  cnptoprest2  15432  lmss  15438  lmtopcnp  15442  neitx  15460  txcnp  15463  txrest  15468  txdis  15469  txlm  15471  cnmpt21  15483  imasnopn  15491  xmetres2  15571  blvalps  15580  blval  15581  bl2in  15595  blhalf  15600  blssps  15619  blss  15620  blssexps  15621  blssex  15622  ssblex  15623  blin2  15624  metss2lem  15689  bdmetval  15692  bdmopn  15696  metrest  15698  xmetxp  15699  xmetxpbl  15700  xmettx  15702  metcnp3  15703  txmetcnp  15710  addcncntoplem  15753  elcncf2  15766  mulc1cncf  15781  cncfco  15783  cncfmet  15784  mulcncf  15800  dedekindeulemub  15810  dedekindeulemloc  15811  dedekindeulemlu  15813  dedekindeu  15815  suplociccex  15817  dedekindicclemub  15819  dedekindicclemloc  15820  dedekindicclemlu  15822  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthdec  15836  ivthreinc  15837  dich0  15844  limcimolemlt  15856  limcimo  15857  cnplimccntop  15862  limccnp2lem  15868  limccnp2cntop  15869  dvfvalap  15873  dvmptfsum  15917  dveflem  15918  plyco  15951  plycn  15954  plyrecj  15955  reeff1olem  15963  reeff1oleme  15964  eflt  15967  sin0pilem2  15975  pilem3  15976  ptolemy  16017  ioocosf1o  16047  logdivlt  16088  logdivle  16089  cxplt  16113  cxple  16114  cxplt3  16117  apcxp2  16136  rprelogbmul  16152  rprelogbdiv  16154  logbgt0b  16163  logbgcd1irrap  16167  zprmlogbap  16179  pellexlem3  16192  efnnfsumcl  16200  ppinprm  16221  chtnprm  16223  efchtqdvds  16226  fsumdvdsmul  16246  chtublem  16256  perfectlem2  16261  bposlem3  16274  lgsdir2lem5  16317  lgsdir  16320  lgsdi  16322  lgsne0  16323  gausslemma2dlem1f1o  16345  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  lgsquad2  16368  2sqlem6  16405  2sqlem10  16410  upgredg  16551  uhgrissubgr  16668  subgrprop3  16669  upgrspanop  16690  umgrspanop  16691  usgrspanop  16692  vtxedgfi  16696  vtxlpfi  16697  upgr2wlkdc  16784  clwwlkccatlem  16807  eupth2lemsfi  16885  depindlem3  16915  nnti  17188  pwtrufal  17193  pwf1oexmid  17195  sssneq  17198  qdencn  17238  cvgcmp2n  17248  trilpolemlt1  17257  trirec0  17260  trirec0xor  17261  qdiff  17265  redc0  17274  reap0  17275  cndcap  17276  nconstwlpolemgt0  17281  neap0mkv  17286  supfz  17288  inffz  17289