Theorem simplr 528

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

Assertion

Ref	Expression
simplr	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad2antlr 489	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

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:  simp1lr  1061  simp2lr  1065  simp3lr  1069  bilukdc  1396  dcun  3535  intab  3875  exmid01  4200  exmidundif  4208  exmidundifim  4209  frirrg  4352  reg2exmidlema  4535  imadiflem  5297  fvco4  5590  fvmptt  5609  fcoconst  5689  f1imass  5777  fcof1  5786  fliftfun  5799  riotass2  5859  ovmpodxf  6002  dftpos4  6266  tfrlem1  6311  tfrlem3ag  6312  tfrlemibacc  6329  tfrlemibfn  6331  tfrlemi1  6335  tfrlemi14d  6336  tfr1onlem3ag  6340  tfr1onlembacc  6345  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfrcllembacc  6358  tfrcllembfn  6360  tfrcllemaccex  6364  frecabcl  6402  nntr2  6506  dcdifsnid  6507  nnm00  6533  ecopovsymg  6636  ecopoverg  6638  th3qlem1  6639  mapss  6693  f1imaen2g  6795  xpen  6847  xpmapenlem  6851  phpm  6867  fidifsnen  6872  dif1enen  6882  fiunsnnn  6883  fin0  6887  fin0or  6888  findcard2d  6893  findcard2sd  6894  diffifi  6896  isinfinf  6899  tridc  6901  fimax2gtrilemstep  6902  fimax2gtri  6903  en2eqpr  6909  onunsnss  6918  unsnfidcex  6921  unsnfidcel  6922  undifdcss  6924  unfiin  6927  fisseneq  6933  ssfirab  6935  f1finf1o  6948  fidcenumlemrks  6954  fidcenumlemrk  6955  fidcenumlemr  6956  fidcenum  6957  suplub2ti  7002  supisolem  7009  ordiso2  7036  djudom  7094  omp1eomlem  7095  difinfsnlem  7100  difinfinf  7102  ctm  7110  ctssdclemn0  7111  enumct  7116  nnnninfeq  7128  nnnninfeq2  7129  nninfisol  7133  enomnilem  7138  finomni  7140  exmidomni  7142  fodju0  7147  ismkvnex  7155  enmkvlem  7161  enwomnilem  7169  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  exmidontriimlem1  7222  exmidontriimlem2  7223  exmidontriimlem3  7224  exmidontriimlem4  7225  exmidontriim  7226  netap  7255  exmidapne  7261  dfplpq2  7355  dfmpq2  7356  mulpipqqs  7374  nqpi  7379  distrnqg  7388  prarloclemarch  7419  enq0tr  7435  nqnq0pi  7439  nq0nn  7443  nnnq0lem1  7447  prarloclemup  7496  prarloclem3  7498  prarloclemcalc  7503  genplt2i  7511  addnqprllem  7528  addnqprulem  7529  appdivnq  7564  distrlem1prl  7583  distrlem1pru  7584  ltaddpr  7598  ltexprlemlol  7603  ltexprlemupu  7605  ltexprlemdisj  7607  addcanprleml  7615  ltaprlem  7619  addextpr  7622  recexprlemopu  7628  recexprlemdisj  7631  recexprlem1ssl  7634  aptiprleml  7640  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemdisj  7652  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemladdfu  7678  caucvgprprlemml  7695  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemexbt  7707  suplocexprlemru  7720  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  prsrlem1  7743  recexgt0sr  7774  mulgt0sr  7779  archsr  7783  caucvgsrlemcau  7794  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  addcnsr  7835  mulcnsr  7836  mulcnsrec  7844  axmulcom  7872  nntopi  7895  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  axsuploc  8032  ltntri  8087  cnegexlem2  8135  cnegexlem3  8136  addsub4  8202  le2add  8403  lt2add  8404  lt2sub  8419  le2sub  8420  rereim  8545  apreim  8562  mulreim  8563  apcotr  8566  apadd1  8567  addext  8569  mulext1  8571  mulext  8573  apti  8581  aptap  8609  receuap  8628  rec11rap  8670  divdivdivap  8672  divadddivap  8686  divsubdivap  8687  rerecclap  8689  recgt0  8809  prodgt0gt0  8810  prodgt0  8811  prodge0  8813  lemulge11  8825  lt2mul2div  8838  ltrec  8842  lerec  8843  ltrec1  8847  lediv2a  8854  mulle0r  8903  sup3exmid  8916  zdiv  9343  eluzuzle  9538  supinfneg  9597  infsupneg  9598  infregelbex  9600  xrltso  9798  xnn0dcle  9804  xnn0letri  9805  npnflt  9817  nmnfgt  9820  z2ge  9828  xaddf  9846  xaddval  9847  xpncan  9873  xleadd1a  9875  xltadd1  9878  xaddge0  9880  xle2add  9881  xleaddadd  9889  ixxss1  9906  ixxss2  9907  elico2  9939  iccsupr  9968  fzass4  10064  fzrev  10086  fz0fzelfz0  10129  fzocatel  10201  elfzomelpfzo  10233  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  qbtwnxr  10260  apbtwnz  10276  btwnzge0  10302  modqid  10351  modqcyc  10361  modqcyc2  10362  modqaddabs  10364  modqaddmod  10365  mulqaddmodid  10366  modqmuladd  10368  modqltm1p1mod  10378  modqsubmod  10384  modqsubmodmod  10385  modaddmodlo  10390  modqmulmod  10391  modqmulmodr  10392  modqsubdir  10395  addmodlteq  10400  iseqf1olemab  10491  iseqf1olemmo  10494  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  exp3val  10524  expcl2lemap  10534  expap0  10552  expnegzap  10556  expmul  10567  leexp1a  10577  qsqeqor  10633  expnbnd  10646  nn0ltexp2  10691  nn0opth2  10706  facndiv  10721  faclbnd  10723  bcval5  10745  bcpasc  10748  hashennnuni  10761  hashunlem  10786  hashunsng  10789  hashprg  10790  fiprsshashgt1  10799  hashxp  10808  fimaxq  10809  zfz1isolemiso  10821  zfz1isolem1  10822  seq3coll  10824  shftlem  10827  shftfvalg  10829  shftfval  10832  2shfti  10842  caucvgrelemrec  10990  caucvgrelemcau  10991  caucvgre  10992  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemcalc3  11027  resqrexlemcvg  11030  resqrexlemglsq  11033  resqrexlemga  11034  sqrtsq  11055  leabs  11085  absexpzap  11091  abslt  11099  absle  11100  abssubap0  11101  caubnd2  11128  icodiamlt  11191  maxleim  11216  maxabslemval  11219  maxleastlt  11226  rexico  11232  zmaxcl  11235  fimaxre2  11237  minmax  11240  xrmaxleim  11254  xrmaxiflemcl  11255  xrmaxifle  11256  xrmaxiflemlub  11258  xrmaxiflemval  11260  xrmaxleastlt  11266  xrmaxltsup  11268  xrmaxadd  11271  xrminmax  11275  xrbdtri  11286  climuni  11303  climshftlemg  11312  iserex  11349  climcau  11357  climrecvg1n  11358  climcvg1nlem  11359  sumeq2  11369  summodclem3  11390  zsumdc  11394  isumss  11401  fisumss  11402  sumsnf  11419  fsumconst  11464  modfsummod  11468  fsum00  11472  fsumabs  11475  fsumrelem  11481  fsumiun  11487  isumsplit  11501  divcnv  11507  geo2sum  11524  geoisumr  11528  cvgratz  11542  ntrivcvgap  11558  prodeq2  11567  prodmodclem2  11587  prodmodc  11588  zproddc  11589  fprodmul  11601  prodsnf  11602  fprodcl2lem  11615  fprodconst  11630  fprodap0  11631  fprodrec  11639  fprodap0f  11646  fprodle  11650  fprodmodd  11651  tanaddap  11749  zdvdsdc  11821  dvds2ln  11833  dvdsle  11852  dvdsext  11863  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  zsupcllemstep  11948  dvdsbnd  11959  gcdsupex  11960  gcdsupcl  11961  dvdslegcd  11967  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemzz  12005  bezoutlembz  12007  bezoutlembi  12008  bezoutlemle  12011  dfgcd3  12013  bezout  12014  dfgcd2  12017  dvdsmulgcd  12028  bezoutr  12035  uzwodc  12040  lcmval  12065  lcmcllem  12069  lcmneg  12076  ncoprmgcdne1b  12091  isprm2lem  12118  prmind2  12122  dvdsnprmd  12127  isprm5  12144  prmdvdsexp  12150  sqrt2irr  12164  oddpwdclemxy  12171  oddpwdclemdc  12175  nonsq  12209  pceu  12297  pcmul  12303  pc2dvds  12331  pcz  12333  pcprmpw2  12334  dvdsprmpweqle  12338  pcfac  12350  qexpz  12352  prmpwdvds  12355  1arith  12367  mul4sq  12394  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemhom  12418  ennnfonelemfun  12420  ennnfonelemf1  12421  ennnfonelemim  12427  exmidunben  12429  ctiunctlemfo  12442  omiunct  12447  ssnnctlemct  12449  isstruct2r  12475  ismgm  12781  issgrp  12814  sgrpidmndm  12826  mndpropd  12846  issubmnd  12848  isgrpinv  12931  grplmulf1o  12949  dfgrp3mlem  12973  grplactcnv  12977  mhmid  12984  mhmmnd  12985  ghmgrp  12987  mulgval  12991  mulgfng  12992  mulgnnp1  12996  mulgnn0dir  13018  mulgneg2  13022  mhmmulg  13029  grpissubg  13059  isnsg  13067  isnsg3  13072  nmzsubg  13075  issrg  13153  srglmhm  13181  srgrmhm  13182  isring  13188  ringadd2  13215  oppr1g  13257  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrd  13268  dvdsrex  13272  dvdsrmul1  13276  unitgrp  13290  subrgintm  13369  subrgpropd  13374  lmodprop2d  13443  lssvsubcl  13457  lssvacl  13466  lssvscl  13467  lsslss  13473  lss1d  13475  opnssneib  13695  restbasg  13707  restopn2  13722  iscnp4  13757  cnss2  13766  cnconst2  13772  cnptopresti  13777  cnptoprest2  13779  neitx  13807  uptx  13813  txrest  13815  txdis1cn  13817  xmetres2  13918  xblss2ps  13943  blhalf  13947  blssps  13966  blss  13967  blssexps  13968  blssex  13969  blin2  13971  metequiv2  14035  bdmetval  14039  metcnp3  14050  metcnp  14051  metcn  14053  metcnpi  14054  metcnpi2  14055  txmetcnp  14057  txmetcn  14058  qtopbas  14061  tgqioo  14086  fsumcncntop  14095  elcncf2  14100  mulcncflem  14129  mulcncf  14130  suplociccreex  14141  limcdifap  14170  cnplimcim  14175  cnplimccntop  14178  limccnpcntop  14183  dvcj  14212  dveflem  14226  reeff1olem  14231  eflt  14235  sin0pilem1  14241  ptolemy  14284  coseq0q4123  14294  coseq0negpitopi  14296  cos02pilt1  14311  cos11  14313  ioocosf1o  14314  cxplt  14375  cxple  14376  cxplt3  14379  apcxp2  14397  rprelogbmul  14412  rprelogbdiv  14414  lgsval  14444  lgsfcl2  14446  lgscllem  14447  lgsval2lem  14450  lgsdir2lem4  14471  lgsdir2lem5  14472  lgsdir2  14473  lgsne0  14478  2sqlem6  14506  2sqlem10  14511  pwle2  14787  pwf1oexmid  14788  subctctexmid  14789  pw1nct  14791  peano4nninf  14794  nninfalllem1  14796  nninfall  14797  nninfsellemeq  14802  nninfsellemqall  14803  sbthom  14813  refeq  14815  isomninnlem  14817  trilpolemeq1  14827  trilpolemlt1  14828  trirec0  14831  apdiff  14835  iswomninnlem  14836  ismkvnnlem  14839  redcwlpolemeq1  14841  ltlenmkv  14857