Theorem simplr 500

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp1lr  1013  simp2lr  1017  simp3lr  1021  bilukdc  1342  dcun  3420  intab  3747  exmid01  4061  exmidundif  4067  exmidundifim  4068  frirrg  4210  reg2exmidlema  4387  imadiflem  5138  fvco4  5425  fvmptt  5444  fcoconst  5523  f1imass  5607  fcof1  5616  fliftfun  5629  riotass2  5688  ovmpodxf  5828  dftpos4  6090  tfrlem1  6135  tfrlem3ag  6136  tfrlemibacc  6153  tfrlemibfn  6155  tfrlemi1  6159  tfrlemi14d  6160  tfr1onlem3ag  6164  tfr1onlembacc  6169  tfr1onlembfn  6171  tfr1onlemaccex  6175  tfrcllembacc  6182  tfrcllembfn  6184  tfrcllemaccex  6188  frecabcl  6226  nntr2  6329  dcdifsnid  6330  nnm00  6355  ecopovsymg  6458  ecopoverg  6460  th3qlem1  6461  mapss  6515  f1imaen2g  6617  xpen  6668  xpmapenlem  6672  phpm  6688  fidifsnen  6693  dif1enen  6703  fiunsnnn  6704  fin0  6708  fin0or  6709  findcard2d  6714  findcard2sd  6715  diffifi  6717  isinfinf  6720  tridc  6722  fimax2gtrilemstep  6723  fimax2gtri  6724  en2eqpr  6730  onunsnss  6734  unsnfidcex  6737  unsnfidcel  6738  undifdcss  6740  unfiin  6743  fisseneq  6749  ssfirab  6750  f1finf1o  6763  fidcenumlemrks  6769  fidcenumlemrk  6770  fidcenumlemr  6771  fidcenum  6772  suplub2ti  6803  supisolem  6810  ordiso2  6835  djudom  6893  omp1eomlem  6894  difinfsnlem  6899  difinfinf  6901  ctm  6909  ctssdclemn0  6910  enumct  6914  enomnilem  6922  finomni  6924  exmidomni  6926  fodju0  6931  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  dfplpq2  7063  dfmpq2  7064  mulpipqqs  7082  nqpi  7087  distrnqg  7096  prarloclemarch  7127  enq0tr  7143  nqnq0pi  7147  nq0nn  7151  nnnq0lem1  7155  prarloclemup  7204  prarloclem3  7206  prarloclemcalc  7211  genplt2i  7219  addnqprllem  7236  addnqprulem  7237  appdivnq  7272  distrlem1prl  7291  distrlem1pru  7292  ltaddpr  7306  ltexprlemlol  7311  ltexprlemupu  7313  ltexprlemdisj  7315  addcanprleml  7323  ltaprlem  7327  addextpr  7330  recexprlemopu  7336  recexprlemdisj  7339  recexprlem1ssl  7342  aptiprleml  7348  cauappcvgprlemm  7354  cauappcvgprlemopl  7355  cauappcvgprlemlol  7356  cauappcvgprlemopu  7357  cauappcvgprlemdisj  7360  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemm  7377  caucvgprlemopl  7378  caucvgprlemlol  7379  caucvgprlemopu  7380  caucvgprlemladdfu  7386  caucvgprprlemml  7403  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemexbt  7415  prsrlem1  7438  recexgt0sr  7469  mulgt0sr  7473  archsr  7477  caucvgsrlemcau  7488  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  addcnsr  7521  mulcnsr  7522  mulcnsrec  7530  axmulcom  7556  nntopi  7579  axcaucvglemcau  7583  axcaucvglemres  7584  ltntri  7761  cnegexlem2  7809  cnegexlem3  7810  addsub4  7876  le2add  8073  lt2add  8074  lt2sub  8089  le2sub  8090  rereim  8214  apreim  8231  mulreim  8232  apcotr  8235  apadd1  8236  addext  8238  mulext1  8240  mulext  8242  apti  8250  receuap  8291  rec11rap  8332  divdivdivap  8334  divadddivap  8348  divsubdivap  8349  rerecclap  8351  recgt0  8466  prodgt0gt0  8467  prodgt0  8468  prodge0  8470  lemulge11  8482  lt2mul2div  8495  ltrec  8499  lerec  8500  ltrec1  8504  lediv2a  8511  mulle0r  8560  sup3exmid  8573  zdiv  8991  eluzuzle  9184  supinfneg  9240  infsupneg  9241  xrltso  9423  npnflt  9439  nmnfgt  9442  z2ge  9450  xaddf  9468  xaddval  9469  xpncan  9495  xleadd1a  9497  xltadd1  9500  xaddge0  9502  xle2add  9503  xleaddadd  9511  ixxss1  9528  ixxss2  9529  elico2  9561  iccsupr  9590  fzass4  9683  fzrev  9705  fz0fzelfz0  9745  fzocatel  9817  elfzomelpfzo  9849  exbtwnzlemstep  9866  rebtwn2zlemstep  9871  qbtwnxr  9876  apbtwnz  9888  btwnzge0  9914  modqid  9963  modqcyc  9973  modqcyc2  9974  modqaddabs  9976  modqaddmod  9977  mulqaddmodid  9978  modqmuladd  9980  modqltm1p1mod  9990  modqsubmod  9996  modqsubmodmod  9997  modaddmodlo  10002  modqmulmod  10003  modqmulmodr  10004  modqsubdir  10007  addmodlteq  10012  iseqf1olemab  10103  iseqf1olemmo  10106  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  exp3val  10136  expcl2lemap  10146  expap0  10164  expnegzap  10168  expmul  10179  leexp1a  10189  expnbnd  10256  nn0opth2  10311  facndiv  10326  faclbnd  10328  bcval5  10350  bcpasc  10353  hashennnuni  10366  hashunlem  10391  hashunsng  10394  hashprg  10395  fiprsshashgt1  10404  hashxp  10413  fimaxq  10414  zfz1isolemiso  10423  zfz1isolem1  10424  seq3coll  10426  shftlem  10429  shftfvalg  10431  shftfval  10434  2shfti  10444  caucvgrelemrec  10591  caucvgrelemcau  10592  caucvgre  10593  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemcalc3  10628  resqrexlemcvg  10631  resqrexlemglsq  10634  resqrexlemga  10635  sqrtsq  10656  leabs  10686  absexpzap  10692  abslt  10700  absle  10701  abssubap0  10702  caubnd2  10729  icodiamlt  10792  maxleim  10817  maxabslemval  10820  maxleastlt  10827  rexico  10833  zmaxcl  10835  fimaxre2  10837  minmax  10840  xrmaxleim  10852  xrmaxiflemcl  10853  xrmaxifle  10854  xrmaxiflemlub  10856  xrmaxiflemval  10858  xrmaxleastlt  10864  xrmaxltsup  10866  xrmaxadd  10869  xrminmax  10873  xrbdtri  10884  climuni  10901  climshftlemg  10910  iserex  10947  climcau  10955  climrecvg1n  10956  climcvg1nlem  10957  sumeq2  10967  summodclem3  10988  zsumdc  10992  isumss  10999  fisumss  11000  sumsnf  11017  fsumconst  11062  modfsummod  11066  fsum00  11070  fsumabs  11073  fsumrelem  11079  fsumiun  11085  isumsplit  11099  divcnv  11105  geo2sum  11122  geoisumr  11126  cvgratz  11140  tanaddap  11244  zdvdsdc  11309  dvds2ln  11321  dvdsle  11337  dvdsext  11348  divalglemeunn  11413  divalglemex  11414  divalglemeuneg  11415  zsupcllemstep  11433  dvdsbnd  11440  gcdsupex  11441  gcdsupcl  11442  dvdslegcd  11448  bezoutlemnewy  11477  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemzz  11483  bezoutlembz  11485  bezoutlembi  11486  bezoutlemle  11489  dfgcd3  11491  bezout  11492  dfgcd2  11495  dvdsmulgcd  11506  bezoutr  11513  lcmval  11537  lcmcllem  11541  lcmneg  11548  ncoprmgcdne1b  11563  isprm2lem  11590  prmind2  11594  dvdsnprmd  11599  prmdvdsexp  11619  sqrt2irr  11633  oddpwdclemxy  11639  oddpwdclemdc  11643  nonsq  11677  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemhom  11720  ennnfonelemfun  11722  ennnfonelemf1  11723  ennnfonelemim  11729  exmidunben  11731  isstruct2r  11752  opnssneib  12107  restbasg  12119  restopn2  12134  iscnp4  12168  cnss2  12177  cnconst2  12183  cnptopresti  12188  cnptoprest2  12190  neitx  12218  uptx  12224  txrest  12226  txdis1cn  12228  xmetres2  12307  xblss2ps  12332  blhalf  12336  blssps  12355  blss  12356  blssexps  12357  blssex  12358  blin2  12360  metequiv2  12424  bdmetval  12428  metcnp3  12435  metcnp  12436  metcn  12438  metcnpi  12439  metcnpi2  12440  qtopbas  12444  tgqioo  12466  elcncf2  12474  mulcncflem  12502  mulcncf  12503  limcdifap  12512  cnplimcim  12516  limccnpcntop  12520  pwle2  12779  pwf1oexmid  12780  peano4nninf  12784  nninfalllemn  12786  nninfalllem1  12787  nninfall  12788  nninfsellemeq  12794  nninfsellemqall  12795  sbthom  12805  refeq  12807  isomninnlem  12809  trilpolemeq1  12817  trilpolemlt1  12818