Theorem simprr 521

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprr	|- ( ( ph /\ ( ps /\ ch ) ) -> ch )

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ch -> ch )
2	1	ad2antll 482	1 |- ( ( ph /\ ( ps /\ ch ) ) -> ch )

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:  simp1rr  1047  simp2rr  1051  simp3rr  1055  disjiun  3924  reg2exmidlema  4449  reg3exmidlemwe  4493  nnsucpred  4530  fvmptt  5512  fcof1  5684  fliftfun  5697  isotr  5717  riotass2  5756  acexmidlemab  5768  ovmpodf  5902  grprinvlem  5965  fnmpoovd  6112  1stconst  6118  2ndconst  6119  cnvf1olem  6121  f1od2  6132  smoiso  6199  tfrcldm  6260  tfrcl  6261  nntr2  6399  swoer  6457  erinxp  6503  ecopovsymg  6528  th3qlem1  6531  f1imaen2g  6687  mapdom1g  6741  fict  6762  fidifsnen  6764  dif1enen  6774  fiunsnnn  6775  fisbth  6777  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fimax2gtri  6795  nnwetri  6804  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  fisseneq  6820  ssfirab  6822  fidcenumlemrk  6842  fidcenumlemr  6843  sbthlemi6  6850  sbthlemi8  6852  isbth  6855  fiuni  6866  supmaxti  6891  infminti  6914  ordiso2  6920  eldju2ndl  6957  eldju2ndr  6958  omp1eomlem  6979  difinfsnlem  6984  difinfinf  6986  ctmlemr  6993  ctssdccl  6996  fodjum  7018  fodju0  7019  exmidfodomrlemrALT  7059  acfun  7063  exmidaclem  7064  ccfunen  7079  dfplpq2  7162  dfmpq2  7163  mulpipqqs  7181  distrnqg  7195  enq0sym  7240  enq0tr  7242  distrnq0  7267  prarloclem3  7305  genplt2i  7318  addlocpr  7344  prmuloc  7374  distrlem1prl  7390  distrlem1pru  7391  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemfl  7417  ltexprlemrl  7418  ltexprlemfu  7419  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  ltaprg  7427  prplnqu  7428  addextpr  7429  recexprlemdisj  7438  recexprlemloc  7439  aptiprleml  7447  aptiprlemu  7448  ltmprr  7450  archpr  7451  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  caucvgprlemnkj  7474  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemdisj  7510  caucvgprprlemloc  7511  caucvgprprlemaddq  7516  suplocexprlemrl  7525  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemex  7530  suplocexprlemub  7531  recexgt0sr  7581  mulgt0sr  7586  prsrriota  7596  suplocsrlem  7616  addcnsr  7642  mulcnsr  7643  mulcnsrec  7651  axmulcom  7679  rereceu  7697  axarch  7699  axcaucvglemres  7707  axpre-suploclemres  7709  lelttr  7852  ltletr  7853  addcan  7942  addcan2  7943  addsub4  8005  ltadd2  8181  le2add  8206  lt2add  8207  lt2sub  8222  le2sub  8223  eqord1  8245  rereim  8348  apreap  8349  apreim  8365  mulreim  8366  apcotr  8369  apadd1  8370  addext  8372  apneg  8373  mulext1  8374  mulext  8376  ltleap  8394  aprcl  8408  mulap0  8415  mulcanapd  8422  rec11ap  8470  rec11rap  8471  divdivdivap  8473  ddcanap  8486  divadddivap  8487  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  lemulge11  8624  lt2mul2div  8637  ltrec  8641  lerec  8642  lerec2  8647  ledivp1  8661  mulle0r  8702  nn0ge0div  9138  suprzclex  9149  qapne  9431  xrlelttr  9589  xrltletr  9590  xrre3  9605  xrrege0  9608  xaddge0  9661  xle2add  9662  xlt2add  9663  fzass4  9842  fzrev  9864  elfz1b  9870  eluzgtdifelfzo  9974  fzocatel  9976  exbtwnzlemex  10027  rebtwn2z  10032  modqid  10122  modqcyc  10132  modqaddabs  10135  modqaddmod  10136  mulqaddmodid  10137  modqadd2mod  10147  modqltm1p1mod  10149  modqsubmod  10155  modqsubmodmod  10156  modaddmodup  10160  modqmulmod  10162  modqmulmodr  10163  modqaddmulmod  10164  modqsubdir  10166  frec2uzisod  10180  uzennn  10209  iseqovex  10229  seqvalcd  10232  seqf  10234  seqovcd  10236  seq3shft2  10246  monoord  10249  iseqf1olemnab  10261  seq3distr  10286  expnegzap  10327  ltexp2a  10345  le2sq2  10368  bernneq  10412  expnlbnd2  10417  nn0opth2  10470  faclbnd  10487  bcval5  10509  hashcl  10527  hashen  10530  fihashdom  10549  hashunlem  10550  hashun  10551  hashxp  10572  fimaxq  10573  zfz1isolem1  10583  zfz1iso  10584  seq3coll  10585  cvg1nlemres  10757  cvg1n  10758  resqrexlemp1rp  10778  resqrexlemoverl  10793  resqrexlemex  10797  sqrtsq  10816  abslt  10860  absle  10861  abs3lem  10883  maxleastlt  10987  maxltsup  10990  fimaxre2  10998  negfi  10999  xrmaxleastlt  11025  xrmaxltsup  11027  xrmaxaddlem  11029  2clim  11070  climcn2  11078  addcn2  11079  mulcn2  11081  reccn2ap  11082  climge0  11094  climcau  11116  summodclem2  11151  summodc  11152  zsumdc  11153  fsumf1o  11159  fisumss  11161  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  mptfzshft  11211  fsumrev  11212  fsummulc2  11217  fsumconst  11223  modfsummod  11227  fsumrelem  11240  binom  11253  cvgratnn  11300  mertenslemub  11303  prodmodclem2  11346  prodmodc  11347  efcllem  11365  tanaddaplem  11445  moddvds  11502  dvdsflip  11549  oexpneg  11574  nn0o  11604  fldivndvdslt  11632  zsupcllemstep  11638  zsupcllemex  11639  zssinfcl  11641  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemeu  11695  dfgcd3  11698  dfgcd2  11702  dvdsmulgcd  11713  bezoutr  11720  lcmgcdlem  11758  coprmdvds2  11774  qredeu  11778  rpdvds  11780  cncongr1  11784  prmind2  11801  isprm6  11825  oddpwdclemdc  11851  nonsq  11885  hashdvds  11897  crth  11900  hashgcdlem  11903  hashgcdeq  11904  ennnfonelemg  11916  ennnfonelemex  11927  ennnfonelemrnh  11929  ennnfonelemf1  11931  ennnfonelemrn  11932  ennnfonelemdm  11933  ennnfonelemim  11937  ennnfone  11938  ctinf  11943  ctiunctlemfo  11952  isstruct2r  11970  setscom  11999  iuncld  12284  ssnei2  12326  topssnei  12331  restopnb  12350  cnfval  12363  cnpfval  12364  iscnp4  12387  cnptopco  12391  cncnpi  12397  cncnp  12399  cnconst2  12402  cnrest2  12405  cnptoprest  12408  cnptoprest2  12409  cnpdis  12411  lmss  12415  lmtopcnp  12419  neitx  12437  txcnp  12440  txrest  12445  txdis1cn  12447  txlm  12448  cnmpt21  12460  imasnopn  12468  xmetres2  12548  blvalps  12557  blval  12558  elbl2ps  12561  elbl2  12562  blhalf  12577  blssexps  12598  blssex  12599  ssblex  12600  blin2  12601  bdmetval  12669  xmetxp  12676  xmettx  12679  metcnpi3  12686  txmetcnp  12687  addcncntoplem  12720  fsumcncntop  12725  elcncf2  12730  mulc1cncf  12745  cncfco  12747  cncfmet  12748  cncfmptc  12751  mulcncf  12760  dedekindeulemub  12765  dedekindeulemloc  12766  dedekindeulemlu  12768  dedekindeu  12770  dedekindicclemub  12774  dedekindicclemloc  12775  dedekindicclemlu  12777  dedekindicclemicc  12779  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimo  12803  cnplimccntop  12808  limccnp2lem  12814  limccnp2cntop  12815  dvfvalap  12819  dveflem  12855  sin0pilem2  12863  pilem3  12864  nnti  13191  pwtrufal  13192  pwf1oexmid  13194  qdencn  13222  cvgcmp2n  13228  trilpolemlt1  13234  supfz  13237  inffz  13238