Theorem simplr 533

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 493	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1lr  1092  simp2lr  1096  simp3lr  1100  bilukdc  1445  dcun  3637  ifnefals  3685  ifeqeqxdc  3687  intab  3999  sn0disj  4127  exmid01  4337  exmidundif  4345  exmidundifim  4346  frirrg  4497  reg2exmidlema  4683  imadiflem  5463  relndmfv  5731  fvco4  5780  fvmptt  5800  fcoconst  5882  funopsn  5894  f1imass  5983  fcof1  5992  fliftfun  6005  riotass2  6070  ovmpodxf  6217  fsuppeq  6491  fsuppeqg  6492  suppssdc  6504  suppssfvg  6507  dftpos4  6538  tfrlem1  6583  tfrlem3ag  6584  tfrlemibacc  6601  tfrlemibfn  6603  tfrlemi1  6607  tfrlemi14d  6608  tfr1onlem3ag  6612  tfr1onlembacc  6617  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfrcllembacc  6630  tfrcllembfn  6632  tfrcllemaccex  6636  frecabcl  6674  nntr2  6780  dcdifsnid  6781  nnm00  6807  ecopovsymg  6912  ecopoverg  6914  th3qlem1  6915  mapss  6978  f1imaen2g  7085  pw2f1odclem  7139  xpen  7150  xpmapenlem  7154  mapunen  7156  phpm  7172  fidifsnen  7177  dif1enen  7189  fiunsnnn  7190  fin0  7194  fin0or  7195  findcard2d  7200  findcard2sd  7201  diffifi  7203  isinfinf  7206  tridc  7209  fimax2gtrilemstep  7210  fimax2gtri  7211  en2eqpr  7219  onunsnss  7229  unsnfidcex  7232  unsnfidcel  7233  undifdcss  7235  unfiin  7238  fisseneq  7247  ssfirab  7249  f1finf1o  7270  fidcenumlemrks  7276  fidcenumlemrk  7277  fidcenumlemr  7278  fidcenum  7279  ffsuppbi  7306  fdcf1  7322  f1setfi  7323  2omap  7325  suplub2ti  7348  supisolem  7355  ordiso2  7382  djudom  7440  omp1eomlem  7441  difinfsnlem  7446  difinfinf  7448  ctm  7456  ctssdclemn0  7457  enumct  7462  nnnninfeq  7475  nnnninfeq2  7476  nninfisol  7480  enomnilem  7485  finomni  7487  exmidomni  7489  fodju0  7494  ismkvnex  7502  enmkvlem  7508  enwomnilem  7516  pr2cv1  7548  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  exmidontriimlem1  7584  exmidontriimlem2  7585  exmidontriimlem3  7586  exmidontriimlem4  7587  exmidontriim  7588  netap  7627  exmidapne  7633  dfplpq2  7728  dfmpq2  7729  mulpipqqs  7747  nqpi  7752  distrnqg  7761  prarloclemarch  7792  enq0tr  7808  nqnq0pi  7812  nq0nn  7816  nnnq0lem1  7820  prarloclemup  7869  prarloclem3  7871  prarloclemcalc  7876  genplt2i  7884  addnqprllem  7901  addnqprulem  7902  appdivnq  7937  distrlem1prl  7956  distrlem1pru  7957  ltaddpr  7971  ltexprlemlol  7976  ltexprlemupu  7978  ltexprlemdisj  7980  addcanprleml  7988  ltaprlem  7992  addextpr  7995  recexprlemopu  8001  recexprlemdisj  8004  recexprlem1ssl  8007  aptiprleml  8013  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemdisj  8025  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemladdfu  8051  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemexbt  8080  suplocexprlemru  8093  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  prsrlem1  8116  recexgt0sr  8147  mulgt0sr  8152  archsr  8156  caucvgsrlemcau  8167  caucvgsrlemoffcau  8172  caucvgsrlemoffres  8174  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  addcnsr  8208  mulcnsr  8209  mulcnsrec  8217  axmulcom  8245  nntopi  8268  axcaucvglemcau  8272  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  mpomulf  8323  axsuploc  8405  ltntri  8462  cnegexlem2  8510  cnegexlem3  8511  addsub4  8577  le2add  8780  lt2add  8781  lt2sub  8796  le2sub  8797  rereim  8923  apreim  8940  mulreim  8941  apcotr  8944  apadd1  8945  addext  8947  mulext1  8949  mulext  8951  apti  8959  aptap  8987  receuap  9008  rec11rap  9050  divdivdivap  9052  divadddivap  9066  divsubdivap  9067  rerecclap  9069  recgt0  9189  prodgt0gt0  9190  prodgt0  9191  prodge0  9193  lemulge11  9205  lt2mul2div  9218  ltrec  9222  lerec  9223  ltrec1  9227  lediv2a  9234  mulle0r  9283  sup3exmid  9296  zdiv  9746  eluzuzle  9947  supinfneg  10012  infsupneg  10013  infregelbex  10015  irraddap  10064  xrltso  10216  xnn0dcle  10222  xnn0letri  10223  npnflt  10235  nmnfgt  10238  z2ge  10246  xaddf  10264  xaddval  10265  xpncan  10291  xleadd1a  10293  xltadd1  10296  xaddge0  10298  xle2add  10299  xleaddadd  10307  ixxss1  10324  ixxss2  10325  elico2  10357  iccsupr  10386  fzass4  10486  fzrev  10509  fz0fzelfz0  10552  fzocatel  10635  elfzomelpfzo  10667  zsupcllemstep  10680  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  qbtwnxr  10710  xqltnle  10720  apbtwnz  10727  flaplt  10740  btwnzge0  10757  modqid  10808  modqcyc  10818  modqcyc2  10819  modqaddabs  10821  modqaddmod  10822  mulqaddmodid  10823  modqmuladd  10825  modqltm1p1mod  10835  modqsubmod  10841  modqsubmodmod  10842  modaddmodlo  10847  modqmulmod  10848  modqmulmodr  10849  modqsubdir  10852  addmodlteq  10857  nninfinf  10902  iseqf1olemab  10961  iseqf1olemmo  10964  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  seqf1oglem1  10978  seqf1oglem2  10979  seqf1og  10980  exp3val  11000  expcl2lemap  11010  expap0  11028  expnegzap  11032  expmul  11043  leexp1a  11053  qsqeqor  11109  resq01  11117  expnbnd  11123  nn0ltexp2  11170  nn0opth2  11185  facndiv  11200  faclbnd  11202  bcval5  11224  bcpasc  11227  hashennnuni  11241  hashunlem  11267  hashunsng  11271  hashprg  11272  fiprsshashgt1  11281  hashxp  11290  fimaxq  11293  hashfibc  11306  zfz1isolemiso  11314  zfz1isolem1  11315  seq3coll  11317  iswrdiz  11334  wrdnval  11358  ccatlen  11386  ccatvalfn  11392  ccatsymb  11393  ccatalpha  11404  ccat2s1fstg  11439  swrdclg  11445  swrdsb0eq  11460  pfxwrdsymbg  11485  wrdind  11517  wrd2ind  11518  swrdccatin2  11524  pfxccatin12lem2  11526  pfxccatin12  11528  pfxccat3  11529  swrdccat  11530  shftlem  11604  shftfvalg  11606  shftfval  11609  2shfti  11619  caucvgrelemrec  11768  caucvgrelemcau  11769  caucvgre  11770  cvg1nlemcau  11773  cvg1nlemres  11774  resqrexlemcalc3  11805  resqrexlemcvg  11808  resqrexlemglsq  11811  resqrexlemga  11812  sqrtsq  11833  leabs  11863  absexpzap  11870  abslt  11878  absle  11879  abssubap0  11880  caubnd2  11907  icodiamlt  11970  maxleim  11995  maxabslemval  11998  maxleastlt  12005  rexico  12011  zmaxcl  12014  fimaxre2  12017  fiidxsupcl  12019  minmax  12021  zmincl  12030  xrmaxleim  12036  xrmaxiflemcl  12037  xrmaxifle  12038  xrmaxiflemlub  12040  xrmaxiflemval  12042  xrmaxleastlt  12048  xrmaxltsup  12050  xrmaxadd  12053  xrminmax  12057  xrbdtri  12068  climuni  12085  climshftlemg  12094  iserex  12131  climcau  12139  climrecvg1n  12140  climcvg1nlem  12141  sumeq2  12151  summodclem3  12173  zsumdc  12177  isumss  12184  fisumss  12185  sumsnf  12202  fsumconst  12247  modfsummod  12251  fsum00  12255  fsumabs  12258  fsumrelem  12264  fsumiun  12270  isumsplit  12284  divcnv  12290  geo2sum  12307  geoisumr  12311  cvgratz  12325  ntrivcvgap  12341  prodeq2  12350  prodmodclem2  12370  prodmodc  12371  zproddc  12372  fprodmul  12384  prodsnf  12385  fprodcl2lem  12398  fprodconst  12413  fprodap0  12414  fprodrec  12422  fprodap0f  12429  fprodle  12433  fprodmodd  12434  tanaddap  12532  zdvdsdc  12605  dvds2ln  12617  fsumdvds  12635  dvdsle  12637  dvdsext  12648  divalglemeunn  12714  divalglemex  12715  divalglemeuneg  12716  bitsfzo  12748  bitsmod  12749  bitsinv1lem  12754  bitsinv1  12755  dvdsbnd  12759  gcdsupex  12760  gcdsupcl  12761  dvdslegcd  12767  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlemzz  12805  bezoutlembz  12807  bezoutlembi  12808  bezoutlemle  12811  dfgcd3  12813  bezout  12814  dfgcd2  12817  dvdsmulgcd  12828  bezoutr  12835  uzwodc  12840  nninfctlemfo  12843  lcmval  12867  lcmcllem  12871  lcmneg  12878  ncoprmgcdne1b  12893  isprm2lem  12920  prmind2  12924  dvdsnprmd  12929  isprm5  12947  prmdvdsexp  12953  sqrt2irr  12967  nonsq  13013  sqrtrirr  13015  pceu  13104  pcmul  13110  pc2dvds  13139  pcz  13141  pcprmpw2  13142  dvdsprmpweqle  13146  pcfac  13159  qexpz  13161  prmpwdvds  13164  1arith  13176  mul4sq  13203  4sqexercise2  13208  4sqlemsdc  13209  ballotfilem2  13287  ballotfilemsle  13307  ballotfilemsdom  13314  ballotfilemsima  13318  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemhom  13365  ennnfonelemfun  13367  ennnfonelemf1  13368  ennnfonelemim  13374  exmidunben  13376  ctiunctlemfo  13389  omiunct  13394  ssnnctlemct  13396  isstruct2r  13422  ismgm  13737  issgrp  13778  sgrppropd  13788  sgrpidmndm  13793  mndpropd  13813  issubmnd  13815  resmhm2b  13856  gzsumwmhm  13863  isgrpinv  13919  grplmulf1o  13939  dfgrp3mlem  13963  grplactcnv  13967  mhmid  13978  mhmmnd  13979  ghmgrp  13981  mulgval  13985  mulgfng  13987  mulgnnp1  13993  mulgnn0dir  14015  mulgneg2  14019  mhmmulg  14026  grpissubg  14057  isnsg  14065  isnsg3  14070  nmzsubg  14073  ghmmhmb  14117  ghmpreima  14129  ghmnsgpreima  14132  ghmf1  14136  ghmf1o  14138  conjghm  14139  conjnmz  14142  conjnmzb  14143  resscntz  14167  cntzsubg  14172  cntrsubgnsg  14176  ghmcmn  14222  gzsumconst  14234  gsumzfi  14249  gsumclfi  14250  gsummptfidmadd  14252  gsumsubmclfi  14254  gsummptfidmsplit  14255  gsumsnfdcmn  14258  gsumresfi  14264  gsumconstcmn  14267  gsum2dfilem2  14273  prdsval  14281  prdsidlem  14301  pwssub  14324  issrg  14377  srglmhm  14405  srgrmhm  14406  isring  14412  ringadd2  14440  ringlghm  14474  ringrghm  14475  oppr1g  14498  dvdsrvald  14510  dvdsrd  14511  dvdsrex  14515  dvdsrmul1  14519  unitgrp  14533  rhmopp  14593  subrgintm  14661  subrgpropd  14671  isdomn  14688  aprnzr  14709  opprdrng  14730  lmodprop2d  14795  lssvacl  14812  lssvsubcl  14813  lssvscl  14822  lsslss  14828  lss1d  14830  lsspropdg  14878  gsumfsum  15033  expghmap  15052  mulgghm2  15053  znunit  15104  znrrg  15105  issubassa2  15145  assamulgscmlem1  15151  assamulgscmlem2  15152  psrass1filem  15182  psrass1fi  15206  mvrffi  15214  mplvalcoe  15218  mplsubgfilemcl  15227  mplsubgfileminv  15228  mplsubgfi  15229  opnssneib  15394  restbasg  15406  restopn2  15421  iscnp4  15456  cnss2  15465  cnconst2  15471  cnptopresti  15476  cnptoprest2  15478  neitx  15506  uptx  15512  txrest  15514  txdis1cn  15516  xmetres2  15617  xblss2ps  15642  blhalf  15646  blssps  15665  blss  15666  blssexps  15667  blssex  15668  blin2  15670  metequiv2  15734  bdmetval  15738  metcnp3  15749  metcnp  15750  metcn  15752  metcnpi  15753  metcnpi2  15754  txmetcnp  15756  txmetcn  15757  qtopbas  15760  tgqioo  15793  mpomulcn  15804  fsumcncntop  15805  elcncf2  15812  mulcncflem  15845  mulcncf  15846  suplociccreex  15862  limcdifap  15900  cnplimcim  15905  cnplimccntop  15908  limccnpcntop  15913  dvcj  15947  dvmptfsum  15963  dveflem  15964  ply1termlem  15980  plyaddlem1  15985  plymullem1  15986  plycolemc  15996  plycjlemc  15998  plyrecj  16001  dvply1  16003  reeff1olem  16009  eflt  16013  sin0pilem1  16020  ptolemy  16063  coseq0q4123  16073  coseq0negpitopi  16075  cos02pilt1  16091  cos11  16093  ioocosf1o  16094  logdivlt  16136  logdivle  16137  rpcxpmul2  16158  rpcxpmul2z  16160  cxplt  16163  cxple  16164  cxplt3  16167  apcxp2  16186  rprelogbmul  16203  rprelogbdiv  16205  birthdaylem3  16239  pellexlem3  16243  ppiqltx  16293  dvdsppwf1o  16295  chtqub  16308  perfect  16313  bcmax  16317  bposlem3  16325  bpos  16332  lgsval  16340  lgsfcl2  16342  lgscllem  16343  lgsval2lem  16346  lgsdir2lem4  16367  lgsdir2lem5  16368  lgsdir2  16369  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  2sqlem6  16456  2sqlem10  16461  umgrnloopv  16572  umgrvad2edg  16669  usgr1eop  16703  wlkvtxiedg  16803  wlkvtxiedgg  16804  upgredginwlk  16814  upgriswlkdc  16818  clwwlkccatlem  16858  eupth2lem3lem4fi  16931  pw1ndom3  17237  pw1map  17242  pwle2  17245  pwf1oexmid  17246  subctctexmid  17247  pw1nct  17250  stnot  17256  peano4nninf  17267  nninfalllem1  17269  nninfall  17270  nninfsellemeq  17275  nninfsellemqall  17276  nnnninfex  17283  nninfnfiinf  17284  sbthom  17289  refeq  17291  isomninnlem  17297  trilpolemeq1  17308  trilpolemlt1  17309  trirec0  17312  apdiff  17316  iswomninnlem  17318  ismkvnnlem  17321  redcwlpolemeq1  17323  ltlenmkv  17339