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  3533  intab  3873  exmid01  4197  exmidundif  4205  exmidundifim  4206  frirrg  4349  reg2exmidlema  4532  imadiflem  5294  fvco4  5587  fvmptt  5606  fcoconst  5686  f1imass  5772  fcof1  5781  fliftfun  5794  riotass2  5854  ovmpodxf  5997  dftpos4  6261  tfrlem1  6306  tfrlem3ag  6307  tfrlemibacc  6324  tfrlemibfn  6326  tfrlemi1  6330  tfrlemi14d  6331  tfr1onlem3ag  6335  tfr1onlembacc  6340  tfr1onlembfn  6342  tfr1onlemaccex  6346  tfrcllembacc  6353  tfrcllembfn  6355  tfrcllemaccex  6359  frecabcl  6397  nntr2  6501  dcdifsnid  6502  nnm00  6528  ecopovsymg  6631  ecopoverg  6633  th3qlem1  6634  mapss  6688  f1imaen2g  6790  xpen  6842  xpmapenlem  6846  phpm  6862  fidifsnen  6867  dif1enen  6877  fiunsnnn  6878  fin0  6882  fin0or  6883  findcard2d  6888  findcard2sd  6889  diffifi  6891  isinfinf  6894  tridc  6896  fimax2gtrilemstep  6897  fimax2gtri  6898  en2eqpr  6904  onunsnss  6913  unsnfidcex  6916  unsnfidcel  6917  undifdcss  6919  unfiin  6922  fisseneq  6928  ssfirab  6930  f1finf1o  6943  fidcenumlemrks  6949  fidcenumlemrk  6950  fidcenumlemr  6951  fidcenum  6952  suplub2ti  6997  supisolem  7004  ordiso2  7031  djudom  7089  omp1eomlem  7090  difinfsnlem  7095  difinfinf  7097  ctm  7105  ctssdclemn0  7106  enumct  7111  nnnninfeq  7123  nnnninfeq2  7124  nninfisol  7128  enomnilem  7133  finomni  7135  exmidomni  7137  fodju0  7142  ismkvnex  7150  enmkvlem  7156  enwomnilem  7164  exmidfodomrlemr  7198  exmidfodomrlemrALT  7199  exmidaclem  7204  exmidontriimlem1  7217  exmidontriimlem2  7218  exmidontriimlem3  7219  exmidontriimlem4  7220  exmidontriim  7221  netap  7250  exmidapne  7256  dfplpq2  7350  dfmpq2  7351  mulpipqqs  7369  nqpi  7374  distrnqg  7383  prarloclemarch  7414  enq0tr  7430  nqnq0pi  7434  nq0nn  7438  nnnq0lem1  7442  prarloclemup  7491  prarloclem3  7493  prarloclemcalc  7498  genplt2i  7506  addnqprllem  7523  addnqprulem  7524  appdivnq  7559  distrlem1prl  7578  distrlem1pru  7579  ltaddpr  7593  ltexprlemlol  7598  ltexprlemupu  7600  ltexprlemdisj  7602  addcanprleml  7610  ltaprlem  7614  addextpr  7617  recexprlemopu  7623  recexprlemdisj  7626  recexprlem1ssl  7629  aptiprleml  7635  cauappcvgprlemm  7641  cauappcvgprlemopl  7642  cauappcvgprlemlol  7643  cauappcvgprlemopu  7644  cauappcvgprlemdisj  7647  cauappcvgprlemladdfu  7650  cauappcvgprlemladdfl  7651  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemm  7664  caucvgprlemopl  7665  caucvgprlemlol  7666  caucvgprlemopu  7667  caucvgprlemladdfu  7673  caucvgprprlemml  7690  caucvgprprlemopl  7693  caucvgprprlemlol  7694  caucvgprprlemopu  7695  caucvgprprlemexbt  7702  suplocexprlemru  7715  suplocexprlemloc  7717  suplocexprlemub  7719  suplocexprlemlub  7720  prsrlem1  7738  recexgt0sr  7769  mulgt0sr  7774  archsr  7778  caucvgsrlemcau  7789  caucvgsrlemoffcau  7794  caucvgsrlemoffres  7796  suplocsrlemb  7802  suplocsrlempr  7803  suplocsrlem  7804  addcnsr  7830  mulcnsr  7831  mulcnsrec  7839  axmulcom  7867  nntopi  7890  axcaucvglemcau  7894  axcaucvglemres  7895  axpre-suploclemres  7897  axpre-suploc  7898  axsuploc  8026  ltntri  8081  cnegexlem2  8129  cnegexlem3  8130  addsub4  8196  le2add  8397  lt2add  8398  lt2sub  8413  le2sub  8414  rereim  8539  apreim  8556  mulreim  8557  apcotr  8560  apadd1  8561  addext  8563  mulext1  8565  mulext  8567  apti  8575  aptap  8603  receuap  8622  rec11rap  8664  divdivdivap  8666  divadddivap  8680  divsubdivap  8681  rerecclap  8683  recgt0  8803  prodgt0gt0  8804  prodgt0  8805  prodge0  8807  lemulge11  8819  lt2mul2div  8832  ltrec  8836  lerec  8837  ltrec1  8841  lediv2a  8848  mulle0r  8897  sup3exmid  8910  zdiv  9337  eluzuzle  9532  supinfneg  9591  infsupneg  9592  infregelbex  9594  xrltso  9792  xnn0dcle  9798  xnn0letri  9799  npnflt  9811  nmnfgt  9814  z2ge  9822  xaddf  9840  xaddval  9841  xpncan  9867  xleadd1a  9869  xltadd1  9872  xaddge0  9874  xle2add  9875  xleaddadd  9883  ixxss1  9900  ixxss2  9901  elico2  9933  iccsupr  9962  fzass4  10057  fzrev  10079  fz0fzelfz0  10122  fzocatel  10194  elfzomelpfzo  10226  exbtwnzlemstep  10243  rebtwn2zlemstep  10248  qbtwnxr  10253  apbtwnz  10269  btwnzge0  10295  modqid  10344  modqcyc  10354  modqcyc2  10355  modqaddabs  10357  modqaddmod  10358  mulqaddmodid  10359  modqmuladd  10361  modqltm1p1mod  10371  modqsubmod  10377  modqsubmodmod  10378  modaddmodlo  10383  modqmulmod  10384  modqmulmodr  10385  modqsubdir  10388  addmodlteq  10393  iseqf1olemab  10484  iseqf1olemmo  10487  iseqf1olemjpcl  10490  iseqf1olemqpcl  10491  exp3val  10517  expcl2lemap  10527  expap0  10545  expnegzap  10549  expmul  10560  leexp1a  10570  qsqeqor  10625  expnbnd  10638  nn0ltexp2  10683  nn0opth2  10697  facndiv  10712  faclbnd  10714  bcval5  10736  bcpasc  10739  hashennnuni  10752  hashunlem  10777  hashunsng  10780  hashprg  10781  fiprsshashgt1  10790  hashxp  10799  fimaxq  10800  zfz1isolemiso  10812  zfz1isolem1  10813  seq3coll  10815  shftlem  10818  shftfvalg  10820  shftfval  10823  2shfti  10833  caucvgrelemrec  10981  caucvgrelemcau  10982  caucvgre  10983  cvg1nlemcau  10986  cvg1nlemres  10987  resqrexlemcalc3  11018  resqrexlemcvg  11021  resqrexlemglsq  11024  resqrexlemga  11025  sqrtsq  11046  leabs  11076  absexpzap  11082  abslt  11090  absle  11091  abssubap0  11092  caubnd2  11119  icodiamlt  11182  maxleim  11207  maxabslemval  11210  maxleastlt  11217  rexico  11223  zmaxcl  11226  fimaxre2  11228  minmax  11231  xrmaxleim  11245  xrmaxiflemcl  11246  xrmaxifle  11247  xrmaxiflemlub  11249  xrmaxiflemval  11251  xrmaxleastlt  11257  xrmaxltsup  11259  xrmaxadd  11262  xrminmax  11266  xrbdtri  11277  climuni  11294  climshftlemg  11303  iserex  11340  climcau  11348  climrecvg1n  11349  climcvg1nlem  11350  sumeq2  11360  summodclem3  11381  zsumdc  11385  isumss  11392  fisumss  11393  sumsnf  11410  fsumconst  11455  modfsummod  11459  fsum00  11463  fsumabs  11466  fsumrelem  11472  fsumiun  11478  isumsplit  11492  divcnv  11498  geo2sum  11515  geoisumr  11519  cvgratz  11533  ntrivcvgap  11549  prodeq2  11558  prodmodclem2  11578  prodmodc  11579  zproddc  11580  fprodmul  11592  prodsnf  11593  fprodcl2lem  11606  fprodconst  11621  fprodap0  11622  fprodrec  11630  fprodap0f  11637  fprodle  11641  fprodmodd  11642  tanaddap  11740  zdvdsdc  11812  dvds2ln  11824  dvdsle  11842  dvdsext  11853  divalglemeunn  11918  divalglemex  11919  divalglemeuneg  11920  zsupcllemstep  11938  dvdsbnd  11949  gcdsupex  11950  gcdsupcl  11951  dvdslegcd  11957  bezoutlemnewy  11989  bezoutlemstep  11990  bezoutlemmain  11991  bezoutlemzz  11995  bezoutlembz  11997  bezoutlembi  11998  bezoutlemle  12001  dfgcd3  12003  bezout  12004  dfgcd2  12007  dvdsmulgcd  12018  bezoutr  12025  uzwodc  12030  lcmval  12055  lcmcllem  12059  lcmneg  12066  ncoprmgcdne1b  12081  isprm2lem  12108  prmind2  12112  dvdsnprmd  12117  isprm5  12134  prmdvdsexp  12140  sqrt2irr  12154  oddpwdclemxy  12161  oddpwdclemdc  12165  nonsq  12199  pceu  12287  pcmul  12293  pc2dvds  12321  pcz  12323  pcprmpw2  12324  dvdsprmpweqle  12328  pcfac  12340  qexpz  12342  prmpwdvds  12345  1arith  12357  mul4sq  12384  ennnfonelemkh  12405  ennnfonelemhf1o  12406  ennnfonelemhom  12408  ennnfonelemfun  12410  ennnfonelemf1  12411  ennnfonelemim  12417  exmidunben  12419  ctiunctlemfo  12432  omiunct  12437  ssnnctlemct  12439  isstruct2r  12465  ismgm  12708  issgrp  12741  sgrpidmndm  12753  mndpropd  12773  issubmnd  12775  isgrpinv  12858  grplmulf1o  12876  dfgrp3mlem  12900  grplactcnv  12904  mhmid  12911  mhmmnd  12912  ghmgrp  12914  mulgval  12918  mulgfng  12919  mulgnnp1  12923  mulgnn0dir  12944  mulgneg2  12948  mhmmulg  12955  grpissubg  12985  isnsg  12993  isnsg3  12998  nmzsubg  13001  issrg  13079  srglmhm  13107  srgrmhm  13108  isring  13114  ringadd2  13141  oppr1g  13183  reldvdsrsrg  13192  dvdsrvald  13193  dvdsrd  13194  dvdsrex  13198  dvdsrmul1  13202  unitgrp  13216  subrgintm  13302  subrgpropd  13307  opnssneib  13527  restbasg  13539  restopn2  13554  iscnp4  13589  cnss2  13598  cnconst2  13604  cnptopresti  13609  cnptoprest2  13611  neitx  13639  uptx  13645  txrest  13647  txdis1cn  13649  xmetres2  13750  xblss2ps  13775  blhalf  13779  blssps  13798  blss  13799  blssexps  13800  blssex  13801  blin2  13803  metequiv2  13867  bdmetval  13871  metcnp3  13882  metcnp  13883  metcn  13885  metcnpi  13886  metcnpi2  13887  txmetcnp  13889  txmetcn  13890  qtopbas  13893  tgqioo  13918  fsumcncntop  13927  elcncf2  13932  mulcncflem  13961  mulcncf  13962  suplociccreex  13973  limcdifap  14002  cnplimcim  14007  cnplimccntop  14010  limccnpcntop  14015  dvcj  14044  dveflem  14058  reeff1olem  14063  eflt  14067  sin0pilem1  14073  ptolemy  14116  coseq0q4123  14126  coseq0negpitopi  14128  cos02pilt1  14143  cos11  14145  ioocosf1o  14146  cxplt  14207  cxple  14208  cxplt3  14211  apcxp2  14229  rprelogbmul  14244  rprelogbdiv  14246  lgsval  14276  lgsfcl2  14278  lgscllem  14279  lgsval2lem  14282  lgsdir2lem4  14303  lgsdir2lem5  14304  lgsdir2  14305  lgsne0  14310  2sqlem6  14327  2sqlem10  14332  pwle2  14608  pwf1oexmid  14609  subctctexmid  14610  pw1nct  14612  peano4nninf  14615  nninfalllem1  14617  nninfall  14618  nninfsellemeq  14623  nninfsellemqall  14624  sbthom  14634  refeq  14636  isomninnlem  14638  trilpolemeq1  14648  trilpolemlt1  14649  trirec0  14652  apdiff  14656  iswomninnlem  14657  ismkvnnlem  14660  redcwlpolemeq1  14662  ltlenmkv  14677