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  8466  addcan  8506  addcan2  8507  addsub4  8569  ltadd2  8747  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  eqord1  8811  rimul  8913  rereim  8914  ltmul1  8920  apreim  8931  mulreim  8932  apcotr  8935  apadd1  8936  addext  8938  apneg  8939  mulext1  8940  mulext  8942  ltleap  8960  aprcl  8974  mulap0  8982  mulcanapd  8989  receuap  8999  recapb  9001  rec11ap  9040  rec11rap  9041  divdivdivap  9043  ddcanap  9056  divadddivap  9057  conjmulap  9059  subrecap  9169  prodgt0gt0  9181  prodge0  9184  ltmul12a  9190  lemulge11  9196  lt2mul2div  9209  ltrec  9213  lerec  9214  lt2msq  9216  lerec2  9219  le2msq  9231  msq11  9232  ledivp1  9233  mulle0r  9274  suprzclex  9744  peano5uzti  9754  supinfneg  9995  infsupneg  9996  qapne  10039  xrlelttr  10208  xrltletr  10209  xrre  10222  xaddge0  10280  xle2add  10281  xlt2add  10282  divelunit  10404  fzass4  10468  fzocatel  10617  zsupcllemstep  10662  zssinfcl  10665  infssfzcldc  10669  infssfzledc  10670  suprzubdc  10671  zsupssdc  10673  suprzcl2dc  10674  exbtwnzlemex  10684  rebtwn2z  10689  qbtwnre  10691  modqid  10786  modqcyc  10796  modqaddabs  10799  modqaddmod  10800  mulqaddmodid  10801  modqadd2mod  10811  modqltm1p1mod  10813  modqsubmod  10819  modqsubmodmod  10820  modqmulmod  10826  modqmulmodr  10827  modqaddmulmod  10828  modqsubdir  10830  frec2uzisod  10844  iseqovex  10895  seqvalcd  10898  seq1g  10900  seqf  10901  seqovcd  10904  seqm1g  10911  seq3fveq2  10912  seq3shft2  10918  seqshft2g  10919  monoord  10922  seq3split  10925  seqsplitg  10926  iseqf1olemnab  10938  seqf1oglem1  10956  seqf1og  10958  seq3id2  10963  seqhomog  10967  seq3distr  10969  expcl2lemap  10988  expnegzap  11010  ltexp2a  11028  le2sq2  11052  nn0ltexp2  11147  nn0opth2  11162  bcval5  11201  hashcl  11220  hashen  11223  fihashdom  11243  hashunlem  11244  hashun  11245  hashmap  11268  fimaxq  11270  hashfibclem  11282  hashfibc  11283  hashf1lem1  11285  hashf1lem2  11286  hashf1  11287  zfz1isolem1  11292  zfz1iso  11293  lencl  11308  sswrd  11313  fstwrdne0  11344  lswlgt0cl  11357  ccatw2s1p1g  11413  ccat2s1fstg  11416  swrdval  11420  wrdind  11494  wrd2ind  11495  swrdccatfn  11496  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  pfxccat3a  11510  reuccatpfxs1  11519  cvg1nlemres  11751  cvg1n  11752  recvguniq  11761  resqrexlemp1rp  11772  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemex  11791  sqrtmul  11801  sqrtsq  11810  absexpzap  11846  absle  11855  abs3lem  11877  amgm2  11884  maxleastlt  11981  maxltsup  11984  fimaxre2  11993  xrmaxleastlt  12022  xrmaxltsup  12024  xrmaxaddlem  12026  climcn2  12075  addcn2  12076  mulcn2  12078  reccn2ap  12079  climcau  12113  summodclem2  12149  summodc  12150  fsumf1o  12157  fisumss  12159  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  fsum2dlemstep  12201  mptfzshft  12209  fsumrev  12210  fsummulc2  12215  modfsummod  12225  fsumrelem  12238  binom  12251  cvgratnn  12298  mertenslemub  12301  prodmodc  12345  zproddc  12346  fprodf1o  12355  fprodssdc  12357  fprodmul  12358  fprodrev  12386  fprod2dlemstep  12389  efcllem  12426  tanaddaplem  12505  dvdsval2  12557  moddvds  12566  dvdsabseq  12614  dvdsflip  12618  oexpneg  12644  fldivndvdslt  12704  bitsfi  12724  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemeu  12784  dfgcd3  12787  bezout  12788  dvdsmulgcd  12802  bezoutr  12809  nninfctlemfo  12817  ialgrlem1st  12820  lcmgcdlem  12855  coprmdvds2  12871  qredeu  12875  rpdvds  12877  isprm5lem  12919  isprm6  12925  pw2dvdslemn  12943  nonsq  12985  crth  13002  eulerthlemh  13009  pclemdc  13067  pcprendvds2  13070  pceu  13074  pcval  13075  pczpre  13076  pcmul  13080  pcqmul  13082  pcqcl  13085  pcid  13103  pcneg  13104  pcgcd1  13107  pc2dvds  13109  pcprmpw2  13112  difsqpwdvds  13117  pcmpt  13122  pockthg  13136  1arith  13146  mul4sq  13173  4sqexercise2  13178  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemg  13294  ennnfonelemex  13305  ennnfonelemrnh  13307  ennnfonelemrn  13310  ennnfonelemdm  13311  ennnfonelemnn0  13313  ennnfonelemim  13315  ennnfone  13316  ctinfomlemom  13318  ctinf  13321  ctiunctlemfo  13330  nninfdclemcl  13339  nninfdclemf  13340  nninfdclemp1  13341  unbendc  13345  isstruct2r  13363  setscom  13392  qusval  13644  ercpbl  13652  opifismgmdc  13691  grpinvalem  13705  grprida  13707  gzsumvalx  13709  gzsumfzval  13711  gzsumval2  13714  sgrppropd  13728  mndpropd  13753  issubmnd  13755  submnd0  13757  mhmf1o  13777  0mhm  13793  resmhm  13794  mhmco  13797  mhmima  13798  mhmeql  13799  gzsumwsubmcl  13801  gzsumcl  13804  grppropd  13822  grpinvid1  13857  grpinvid2  13858  grplcan  13867  grplmulf1o  13879  grpnpncan0  13901  dfgrp3mlem  13903  grplactcnv  13907  mulgval  13925  mulgfng  13927  mulg1  13932  mulgnnp1  13933  mulgneg  13943  mulgnndir  13954  mulgdirlem  13956  mulgnn0ass  13961  mulgass  13962  subgmulg  13991  issubg4m  13996  subgintm  14001  0nsg  14017  eqgcpbl  14031  ghmmulg  14059  ghmpreima  14069  ghmeql  14070  ghmnsgima  14071  ghmnsgpreima  14072  ghmf1  14076  ghmf1o  14078  conjghm  14079  conjnmzb  14083  qusghm  14085  cmnsubm  14112  ablpncan3  14121  invghm  14133  eqgabl  14134  qusecsub  14135  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gsumvalfi  14152  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  prdssgrpd  14191  prdsmndd  14194  pwssub  14216  imasrng  14255  qusrng  14257  srglmhm  14297  srgrmhm  14298  ringpropd  14343  ringlghm  14366  ringrghm  14367  imasring  14369  qusring2  14371  opprrngbg  14383  dvdsrvald  14400  dvdsrd  14401  dvdsrex  14405  dvdsrtr  14408  unitgrp  14423  unitpropdg  14455  rhmopp  14483  isnzr2  14491  issubrng2  14518  subrngintm  14520  subrgintm  14551  rhmpropd  14562  ringunitap  14593  aprap  14598  drngunitap  14608  lmodprop2d  14685  rmodislmodlem  14687  lssvacl  14702  lssvsubcl  14703  lssvscl  14712  islss3  14716  lsspropdg  14768  rnglidlmcl  14817  2idlcpblrng  14860  crngridl  14867  gsumfsum  14923  expghmap  14942  mulgghm2  14943  mulgrhm  14944  znf1o  14986  znleval  14988  znidom  14992  issubassa3  15012  assapropd  15014  asclghm  15025  issubassa2  15035  psrval  15050  psrbagcon  15062  psrbagconf1o  15064  mplsubgfilemcl  15090  epttop  15191  topssnei  15263  restbasg  15269  restopnb  15282  cnfval  15295  cnpfval  15296  iscnp4  15319  cnpnei  15320  cnptopco  15323  cncnp  15331  cnrest2  15337  cnptoprest  15340  cnptoprest2  15341  lmss  15347  lmtopcnp  15351  neitx  15369  txcnp  15372  txrest  15377  txdis  15378  txlm  15380  cnmpt21  15392  imasnopn  15400  xmetres2  15480  blvalps  15489  blval  15490  bl2in  15504  blhalf  15509  blssps  15528  blss  15529  blssexps  15530  blssex  15531  ssblex  15532  blin2  15533  metss2lem  15598  bdmetval  15601  bdmopn  15605  metrest  15607  xmetxp  15608  xmetxpbl  15609  xmettx  15611  metcnp3  15612  txmetcnp  15619  addcncntoplem  15662  elcncf2  15675  mulc1cncf  15690  cncfco  15692  cncfmet  15693  mulcncf  15709  dedekindeulemub  15719  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeu  15724  suplociccex  15726  dedekindicclemub  15728  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthdec  15745  ivthreinc  15746  dich0  15753  limcimolemlt  15765  limcimo  15766  cnplimccntop  15771  limccnp2lem  15777  limccnp2cntop  15778  dvfvalap  15782  dvmptfsum  15826  dveflem  15827  plyco  15860  plycn  15863  plyrecj  15864  reeff1olem  15872  reeff1oleme  15873  eflt  15876  sin0pilem2  15883  pilem3  15884  ptolemy  15925  ioocosf1o  15955  cxplt  16018  cxple  16019  cxplt3  16022  apcxp2  16041  rprelogbmul  16057  rprelogbdiv  16059  logbgt0b  16068  logbgcd1irrap  16072  pellexlem3  16093  fsumdvdsmul  16105  perfectlem2  16114  lgsdir2lem5  16151  lgsdir  16154  lgsdi  16156  lgsne0  16157  gausslemma2dlem1f1o  16179  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  lgsquad2  16202  2sqlem6  16239  2sqlem10  16244  upgredg  16385  uhgrissubgr  16502  subgrprop3  16503  upgrspanop  16524  umgrspanop  16525  usgrspanop  16526  vtxedgfi  16530  vtxlpfi  16531  upgr2wlkdc  16618  clwwlkccatlem  16641  eupth2lemsfi  16719  depindlem3  16749  nnti  17022  pwtrufal  17027  pwf1oexmid  17029  sssneq  17032  qdencn  17072  cvgcmp2n  17082  trilpolemlt1  17090  trirec0  17093  trirec0xor  17094  qdiff  17098  redc0  17107  reap0  17108  cndcap  17109  nconstwlpolemgt0  17114  neap0mkv  17119  supfz  17121  inffz  17122