Theorem simprl 529

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 490	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:  simp1rl  1062  simp2rl  1066  simp3rl  1070  rmob  3057  disjiun  4000  reg3exmidlemwe  4580  0xp  4708  imainss  5046  iotam  5210  fvmptt  5609  fcof1o  5792  isotr  5819  riota5f  5857  ovmpodf  6008  unielxp  6177  fnmpoovd  6218  1stconst  6224  2ndconst  6225  cnvf1olem  6227  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemres  6352  tfrcllemres  6365  tfrcldm  6366  frecabcl  6402  nnaordi  6511  swoer  6565  qliftfun  6619  ecopovsymg  6636  th3qlem1  6639  mapen  6848  mapxpen  6850  fidifsnen  6872  fisbth  6885  findcard2d  6893  findcard2sd  6894  diffisn  6895  diffifi  6896  ac6sfi  6900  fimax2gtri  6903  fientri3  6916  nnwetri  6917  unsnfi  6920  unsnfidcex  6921  unsnfidcel  6922  fisseneq  6933  fidcenumlemrk  6955  fidcenumlemr  6956  isbth  6968  ordiso2  7036  difinfsnlem  7100  difinfinf  7102  ctmlemr  7109  ctssdccl  7112  fodjum  7146  fodju0  7147  omniwomnimkv  7167  exmidfodomrlemrALT  7204  netap  7255  exmidmotap  7262  cc1  7266  cc2lem  7267  cc3  7269  cc4f  7270  cc4n  7272  dfplpq2  7355  dfmpq2  7356  mulpipqqs  7374  distrnqg  7388  ltexnqq  7409  subhalfnqq  7415  distrnq0  7460  prarloclemup  7496  prarloclem3  7498  prarloc  7504  genplt2i  7511  nqprl  7552  nqpru  7553  prmuloc  7567  mullocpr  7572  distrlem4prl  7585  distrlem4pru  7586  ltaddpr  7598  ltexprlemopl  7602  ltexprlemlol  7603  ltexprlemopu  7604  ltexprlemupu  7605  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  ltaprlem  7619  ltaprg  7620  prplnqu  7621  addextpr  7622  recexprlemdisj  7631  recexprlemloc  7632  recexprlem1ssl  7634  aptiprleml  7640  aptiprlemu  7641  ltmprr  7643  archpr  7644  cauappcvgprlemopl  7647  cauappcvgprlemopu  7649  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlem1  7660  cauappcvgprlem2  7661  cauappcvgprlemlim  7662  caucvgprlemnkj  7667  caucvgprlemopl  7670  caucvgprlemopu  7672  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlem2  7681  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  caucvgprprlemnjltk  7692  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemopu  7700  caucvgprprlemdisj  7703  caucvgprprlemloc  7704  caucvgprprlemexbt  7707  caucvgprprlemaddq  7709  caucvgprprlem2  7711  suplocexprlemrl  7718  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemex  7723  suplocexprlemub  7724  suplocexprlemlub  7725  recexgt0sr  7774  mulgt0sr  7779  prsrriota  7789  caucvgsrlemoffres  7801  suplocsrlem  7809  cnm  7833  addcnsr  7835  mulcnsr  7836  mulcnsrec  7844  axaddcl  7865  axmulcl  7867  axmulcom  7872  rereceu  7890  recriota  7891  axcaucvglemres  7900  axpre-suploclemres  7902  lelttr  8048  ltletr  8049  readdcan  8099  addcan  8139  addcan2  8140  addsub4  8202  ltadd2  8378  le2add  8403  lt2add  8404  lt2sub  8419  le2sub  8420  eqord1  8442  rimul  8544  rereim  8545  ltmul1  8551  apreim  8562  mulreim  8563  apcotr  8566  apadd1  8567  addext  8569  apneg  8570  mulext1  8571  mulext  8573  ltleap  8591  aprcl  8605  mulap0  8613  mulcanapd  8620  receuap  8628  recapb  8630  rec11ap  8669  rec11rap  8670  divdivdivap  8672  ddcanap  8685  divadddivap  8686  conjmulap  8688  subrecap  8798  prodgt0gt0  8810  prodge0  8813  ltmul12a  8819  lemulge11  8825  lt2mul2div  8838  ltrec  8842  lerec  8843  lt2msq  8845  lerec2  8848  le2msq  8860  msq11  8861  ledivp1  8862  mulle0r  8903  suprzclex  9353  peano5uzti  9363  supinfneg  9597  infsupneg  9598  qapne  9641  xrlelttr  9808  xrltletr  9809  xrre  9822  xaddge0  9880  xle2add  9881  xlt2add  9882  divelunit  10004  fzass4  10064  fzocatel  10201  exbtwnzlemex  10252  rebtwn2z  10257  qbtwnre  10259  modqid  10351  modqcyc  10361  modqaddabs  10364  modqaddmod  10365  mulqaddmodid  10366  modqadd2mod  10376  modqltm1p1mod  10378  modqsubmod  10384  modqsubmodmod  10385  modqmulmod  10391  modqmulmodr  10392  modqaddmulmod  10393  modqsubdir  10395  frec2uzisod  10409  iseqovex  10458  seqvalcd  10461  seqf  10463  seqovcd  10465  seq3fveq2  10471  seq3shft2  10475  monoord  10478  seq3split  10481  iseqf1olemnab  10490  seq3id2  10511  seq3distr  10515  expcl2lemap  10534  expnegzap  10556  ltexp2a  10574  le2sq2  10598  nn0ltexp2  10691  nn0opth2  10706  bcval5  10745  hashcl  10763  hashen  10766  fihashdom  10785  hashunlem  10786  hashun  10787  fimaxq  10809  zfz1isolem1  10822  zfz1iso  10823  cvg1nlemres  10996  cvg1n  10997  recvguniq  11006  resqrexlemp1rp  11017  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemex  11036  sqrtmul  11046  sqrtsq  11055  absexpzap  11091  absle  11100  abs3lem  11122  amgm2  11129  maxleastlt  11226  maxltsup  11229  fimaxre2  11237  xrmaxleastlt  11266  xrmaxltsup  11268  xrmaxaddlem  11270  climcn2  11319  addcn2  11320  mulcn2  11322  reccn2ap  11323  climcau  11357  summodclem2  11392  summodc  11393  fsumf1o  11400  fisumss  11402  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  fsum2dlemstep  11444  mptfzshft  11452  fsumrev  11453  fsummulc2  11458  modfsummod  11468  fsumrelem  11481  binom  11494  cvgratnn  11541  mertenslemub  11544  prodmodc  11588  zproddc  11589  fprodf1o  11598  fprodssdc  11600  fprodmul  11601  fprodrev  11629  fprod2dlemstep  11632  efcllem  11669  tanaddaplem  11748  dvdsval2  11799  moddvds  11808  dvdsabseq  11855  dvdsflip  11859  oexpneg  11884  fldivndvdslt  11942  zsupcllemstep  11948  zssinfcl  11951  suprzubdc  11955  zsupssdc  11957  suprzcl2dc  11958  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemeu  12010  dfgcd3  12013  bezout  12014  dvdsmulgcd  12028  bezoutr  12035  ialgrlem1st  12044  lcmgcdlem  12079  coprmdvds2  12095  qredeu  12099  rpdvds  12101  isprm5lem  12143  isprm6  12149  pw2dvdslemn  12167  nonsq  12209  crth  12226  eulerthlemh  12233  pclemdc  12290  pcprendvds2  12293  pceu  12297  pcval  12298  pczpre  12299  pcmul  12303  pcqmul  12305  pcqcl  12308  pcid  12325  pcneg  12326  pcgcd1  12329  pc2dvds  12331  pcprmpw2  12334  difsqpwdvds  12339  pcmpt  12343  pockthg  12357  1arith  12367  mul4sq  12394  ennnfonelemg  12406  ennnfonelemex  12417  ennnfonelemrnh  12419  ennnfonelemrn  12422  ennnfonelemdm  12423  ennnfonelemnn0  12425  ennnfonelemim  12427  ennnfone  12428  ctinfomlemom  12430  ctinf  12433  ctiunctlemfo  12442  nninfdclemcl  12451  nninfdclemf  12452  nninfdclemp1  12453  unbendc  12457  isstruct2r  12475  setscom  12504  qusval  12749  ercpbl  12755  opifismgmdc  12795  grprinvlem  12809  grpridd  12811  mndpropd  12846  issubmnd  12848  submnd0  12850  mhmf1o  12866  0mhm  12878  mhmco  12879  mhmima  12880  mhmeql  12881  grppropd  12898  grpinvid1  12929  grpinvid2  12930  grplcan  12937  grplmulf1o  12949  grpnpncan0  12971  dfgrp3mlem  12973  grplactcnv  12977  mulgval  12991  mulgfng  12992  mulg1  12995  mulgnnp1  12996  mulgneg  13006  mulgnndir  13017  mulgdirlem  13019  mulgnn0ass  13024  mulgass  13025  subgmulg  13053  issubg4m  13058  subgintm  13063  0nsg  13079  eqgcpbl  13092  ablpncan3  13125  srglmhm  13181  srgrmhm  13182  ringpropd  13222  dvdsrvald  13267  dvdsrd  13268  dvdsrex  13272  dvdsrtr  13275  unitgrp  13290  unitpropdg  13322  subrgintm  13369  aprap  13381  lmodprop2d  13443  rmodislmodlem  13445  lssvsubcl  13457  lssvacl  13466  lssvscl  13467  islss3  13471  epttop  13629  topssnei  13701  restbasg  13707  restopnb  13720  cnfval  13733  cnpfval  13734  iscnp4  13757  cnpnei  13758  cnptopco  13761  cncnp  13769  cnrest2  13775  cnptoprest  13778  cnptoprest2  13779  lmss  13785  lmtopcnp  13789  neitx  13807  txcnp  13810  txrest  13815  txdis  13816  txlm  13818  cnmpt21  13830  imasnopn  13838  xmetres2  13918  blvalps  13927  blval  13928  bl2in  13942  blhalf  13947  blssps  13966  blss  13967  blssexps  13968  blssex  13969  ssblex  13970  blin2  13971  metss2lem  14036  bdmetval  14039  bdmopn  14043  metrest  14045  xmetxp  14046  xmetxpbl  14047  xmettx  14049  metcnp3  14050  txmetcnp  14057  addcncntoplem  14090  elcncf2  14100  mulc1cncf  14115  cncfco  14117  cncfmet  14118  mulcncf  14130  dedekindeulemub  14135  dedekindeulemloc  14136  dedekindeulemlu  14138  dedekindeu  14140  suplociccex  14142  dedekindicclemub  14144  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemuopn  14155  ivthdec  14161  limcimolemlt  14172  limcimo  14173  cnplimccntop  14178  limccnp2lem  14184  limccnp2cntop  14185  dvfvalap  14189  dveflem  14226  reeff1olem  14231  reeff1oleme  14232  eflt  14235  sin0pilem2  14242  pilem3  14243  ptolemy  14284  ioocosf1o  14314  cxplt  14375  cxple  14376  cxplt3  14379  apcxp2  14397  rprelogbmul  14412  rprelogbdiv  14414  logbgt0b  14423  logbgcd1irrap  14427  lgsdir2lem5  14472  lgsdir  14475  lgsdi  14477  lgsne0  14478  lgseisenlem2  14490  2sqlem6  14506  2sqlem10  14511  nnti  14783  pwtrufal  14786  pwf1oexmid  14788  sssneq  14790  qdencn  14814  cvgcmp2n  14820  trilpolemlt1  14828  trirec0  14831  trirec0xor  14832  redc0  14844  reap0  14845  nconstwlpolemgt0  14850  neap0mkv  14855  supfz  14857  inffz  14858