Theorem simprl 520

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 481	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp1rl  1046  simp2rl  1050  simp3rl  1054  rmob  3001  disjiun  3924  reg3exmidlemwe  4493  0xp  4619  imainss  4954  fvmptt  5512  fcof1o  5690  isotr  5717  riota5f  5754  ovmpodf  5902  grprinvlem  5965  grpridd  5967  unielxp  6072  fnmpoovd  6112  1stconst  6118  2ndconst  6119  cnvf1olem  6121  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemres  6246  tfrcllemres  6259  tfrcldm  6260  frecabcl  6296  nnaordi  6404  swoer  6457  qliftfun  6511  ecopovsymg  6528  th3qlem1  6531  mapen  6740  mapxpen  6742  fidifsnen  6764  fisbth  6777  findcard2d  6785  findcard2sd  6786  diffisn  6787  diffifi  6788  ac6sfi  6792  fimax2gtri  6795  fientri3  6803  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  fidcenumlemrk  6842  fidcenumlemr  6843  isbth  6855  ordiso2  6920  difinfsnlem  6984  difinfinf  6986  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  exmidfodomrlemrALT  7059  dfplpq2  7162  dfmpq2  7163  mulpipqqs  7181  distrnqg  7195  ltexnqq  7216  subhalfnqq  7222  distrnq0  7267  prarloclemup  7303  prarloclem3  7305  prarloc  7311  genplt2i  7318  nqprl  7359  nqpru  7360  prmuloc  7374  mullocpr  7379  distrlem4prl  7392  distrlem4pru  7393  ltaddpr  7405  ltexprlemopl  7409  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltaprlem  7426  ltaprg  7427  prplnqu  7428  addextpr  7429  recexprlemdisj  7438  recexprlemloc  7439  recexprlem1ssl  7441  aptiprleml  7447  aptiprlemu  7448  ltmprr  7450  archpr  7451  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlem1  7467  cauappcvgprlem2  7468  cauappcvgprlemlim  7469  caucvgprlemnkj  7474  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlem2  7488  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemdisj  7510  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  caucvgprprlem2  7518  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemub  7531  suplocexprlemlub  7532  recexgt0sr  7581  mulgt0sr  7586  prsrriota  7596  caucvgsrlemoffres  7608  suplocsrlem  7616  cnm  7640  addcnsr  7642  mulcnsr  7643  mulcnsrec  7651  axaddcl  7672  axmulcl  7674  axmulcom  7679  rereceu  7697  recriota  7698  axcaucvglemres  7707  axpre-suploclemres  7709  lelttr  7852  ltletr  7853  readdcan  7902  addcan  7942  addcan2  7943  addsub4  8005  ltadd2  8181  le2add  8206  lt2add  8207  lt2sub  8222  le2sub  8223  eqord1  8245  rimul  8347  rereim  8348  ltmul1  8354  apreim  8365  mulreim  8366  apcotr  8369  apadd1  8370  addext  8372  apneg  8373  mulext1  8374  mulext  8376  ltleap  8394  aprcl  8408  mulap0  8415  mulcanapd  8422  receuap  8430  rec11ap  8470  rec11rap  8471  divdivdivap  8473  ddcanap  8486  divadddivap  8487  conjmulap  8489  subrecap  8598  prodgt0gt0  8609  prodge0  8612  ltmul12a  8618  lemulge11  8624  lt2mul2div  8637  ltrec  8641  lerec  8642  lt2msq  8644  lerec2  8647  le2msq  8659  msq11  8660  ledivp1  8661  mulle0r  8702  suprzclex  9149  peano5uzti  9159  supinfneg  9390  infsupneg  9391  qapne  9431  xrlelttr  9589  xrltletr  9590  xrre  9603  xaddge0  9661  xle2add  9662  xlt2add  9663  divelunit  9785  fzass4  9842  fzocatel  9976  exbtwnzlemex  10027  rebtwn2z  10032  qbtwnre  10034  modqid  10122  modqcyc  10132  modqaddabs  10135  modqaddmod  10136  mulqaddmodid  10137  modqadd2mod  10147  modqltm1p1mod  10149  modqsubmod  10155  modqsubmodmod  10156  modqmulmod  10162  modqmulmodr  10163  modqaddmulmod  10164  modqsubdir  10166  frec2uzisod  10180  iseqovex  10229  seqvalcd  10232  seqf  10234  seqovcd  10236  seq3fveq2  10242  seq3shft2  10246  monoord  10249  seq3split  10252  iseqf1olemnab  10261  seq3id2  10282  seq3distr  10286  expcl2lemap  10305  expnegzap  10327  ltexp2a  10345  le2sq2  10368  nn0opth2  10470  bcval5  10509  hashcl  10527  hashen  10530  fihashdom  10549  hashunlem  10550  hashun  10551  fimaxq  10573  zfz1isolem1  10583  zfz1iso  10584  cvg1nlemres  10757  cvg1n  10758  recvguniq  10767  resqrexlemp1rp  10778  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemex  10797  sqrtmul  10807  sqrtsq  10816  absexpzap  10852  absle  10861  abs3lem  10883  amgm2  10890  maxleastlt  10987  maxltsup  10990  fimaxre2  10998  xrmaxleastlt  11025  xrmaxltsup  11027  xrmaxaddlem  11029  climcn2  11078  addcn2  11079  mulcn2  11081  reccn2ap  11082  climcau  11116  summodclem2  11151  summodc  11152  fsumf1o  11159  fisumss  11161  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  fsum2dlemstep  11203  mptfzshft  11211  fsumrev  11212  fsummulc2  11217  modfsummod  11227  fsumrelem  11240  binom  11253  cvgratnn  11300  mertenslemub  11303  prodmodc  11347  efcllem  11365  tanaddaplem  11445  dvdsval2  11496  moddvds  11502  dvdsabseq  11545  dvdsflip  11549  oexpneg  11574  fldivndvdslt  11632  zsupcllemstep  11638  zssinfcl  11641  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemeu  11695  dfgcd3  11698  bezout  11699  dvdsmulgcd  11713  bezoutr  11720  ialgrlem1st  11723  lcmgcdlem  11758  coprmdvds2  11774  qredeu  11778  rpdvds  11780  isprm6  11825  pw2dvdslemn  11843  nonsq  11885  crth  11900  ennnfonelemg  11916  ennnfonelemex  11927  ennnfonelemrnh  11929  ennnfonelemrn  11932  ennnfonelemdm  11933  ennnfonelemnn0  11935  ennnfonelemim  11937  ennnfone  11938  ctinfomlemom  11940  ctinf  11943  ctiunctlemfo  11952  isstruct2r  11970  setscom  11999  epttop  12259  topssnei  12331  restbasg  12337  restopnb  12350  cnfval  12363  cnpfval  12364  iscnp4  12387  cnpnei  12388  cnptopco  12391  cncnp  12399  cnrest2  12405  cnptoprest  12408  cnptoprest2  12409  lmss  12415  lmtopcnp  12419  neitx  12437  txcnp  12440  txrest  12445  txdis  12446  txlm  12448  cnmpt21  12460  imasnopn  12468  xmetres2  12548  blvalps  12557  blval  12558  bl2in  12572  blhalf  12577  blssps  12596  blss  12597  blssexps  12598  blssex  12599  ssblex  12600  blin2  12601  metss2lem  12666  bdmetval  12669  bdmopn  12673  metrest  12675  xmetxp  12676  xmetxpbl  12677  xmettx  12679  metcnp3  12680  txmetcnp  12687  addcncntoplem  12720  elcncf2  12730  mulc1cncf  12745  cncfco  12747  cncfmet  12748  mulcncf  12760  dedekindeulemub  12765  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeu  12770  suplociccex  12772  dedekindicclemub  12774  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthdec  12791  limcimolemlt  12802  limcimo  12803  cnplimccntop  12808  limccnp2lem  12814  limccnp2cntop  12815  dvfvalap  12819  dveflem  12855  sin0pilem2  12863  pilem3  12864  ptolemy  12905  nnti  13191  pwtrufal  13192  pwf1oexmid  13194  qdencn  13222  cvgcmp2n  13228  trilpolemlt1  13234  supfz  13237  inffz  13238