Theorem simplr 519

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

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:  simp1lr  1045  simp2lr  1049  simp3lr  1053  bilukdc  1374  dcun  3473  intab  3800  exmid01  4121  exmidundif  4129  exmidundifim  4130  frirrg  4272  reg2exmidlema  4449  imadiflem  5202  fvco4  5493  fvmptt  5512  fcoconst  5591  f1imass  5675  fcof1  5684  fliftfun  5697  riotass2  5756  ovmpodxf  5896  dftpos4  6160  tfrlem1  6205  tfrlem3ag  6206  tfrlemibacc  6223  tfrlemibfn  6225  tfrlemi1  6229  tfrlemi14d  6230  tfr1onlem3ag  6234  tfr1onlembacc  6239  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfrcllembacc  6252  tfrcllembfn  6254  tfrcllemaccex  6258  frecabcl  6296  nntr2  6399  dcdifsnid  6400  nnm00  6425  ecopovsymg  6528  ecopoverg  6530  th3qlem1  6531  mapss  6585  f1imaen2g  6687  xpen  6739  xpmapenlem  6743  phpm  6759  fidifsnen  6764  dif1enen  6774  fiunsnnn  6775  fin0  6779  fin0or  6780  findcard2d  6785  findcard2sd  6786  diffifi  6788  isinfinf  6791  tridc  6793  fimax2gtrilemstep  6794  fimax2gtri  6795  en2eqpr  6801  onunsnss  6805  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  unfiin  6814  fisseneq  6820  ssfirab  6822  f1finf1o  6835  fidcenumlemrks  6841  fidcenumlemrk  6842  fidcenumlemr  6843  fidcenum  6844  suplub2ti  6888  supisolem  6895  ordiso2  6920  djudom  6978  omp1eomlem  6979  difinfsnlem  6984  difinfinf  6986  ctm  6994  ctssdclemn0  6995  enumct  7000  enomnilem  7010  finomni  7012  exmidomni  7014  fodju0  7019  ismkvnex  7029  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  dfplpq2  7162  dfmpq2  7163  mulpipqqs  7181  nqpi  7186  distrnqg  7195  prarloclemarch  7226  enq0tr  7242  nqnq0pi  7246  nq0nn  7250  nnnq0lem1  7254  prarloclemup  7303  prarloclem3  7305  prarloclemcalc  7310  genplt2i  7318  addnqprllem  7335  addnqprulem  7336  appdivnq  7371  distrlem1prl  7390  distrlem1pru  7391  ltaddpr  7405  ltexprlemlol  7410  ltexprlemupu  7412  ltexprlemdisj  7414  addcanprleml  7422  ltaprlem  7426  addextpr  7429  recexprlemopu  7435  recexprlemdisj  7438  recexprlem1ssl  7441  aptiprleml  7447  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemdisj  7459  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemladdfu  7485  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemexbt  7514  suplocexprlemru  7527  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  prsrlem1  7550  recexgt0sr  7581  mulgt0sr  7586  archsr  7590  caucvgsrlemcau  7601  caucvgsrlemoffcau  7606  caucvgsrlemoffres  7608  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  addcnsr  7642  mulcnsr  7643  mulcnsrec  7651  axmulcom  7679  nntopi  7702  axcaucvglemcau  7706  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  axsuploc  7837  ltntri  7890  cnegexlem2  7938  cnegexlem3  7939  addsub4  8005  le2add  8206  lt2add  8207  lt2sub  8222  le2sub  8223  rereim  8348  apreim  8365  mulreim  8366  apcotr  8369  apadd1  8370  addext  8372  mulext1  8374  mulext  8376  apti  8384  receuap  8430  rec11rap  8471  divdivdivap  8473  divadddivap  8487  divsubdivap  8488  rerecclap  8490  recgt0  8608  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  lemulge11  8624  lt2mul2div  8637  ltrec  8641  lerec  8642  ltrec1  8646  lediv2a  8653  mulle0r  8702  sup3exmid  8715  zdiv  9139  eluzuzle  9334  supinfneg  9390  infsupneg  9391  xrltso  9582  npnflt  9598  nmnfgt  9601  z2ge  9609  xaddf  9627  xaddval  9628  xpncan  9654  xleadd1a  9656  xltadd1  9659  xaddge0  9661  xle2add  9662  xleaddadd  9670  ixxss1  9687  ixxss2  9688  elico2  9720  iccsupr  9749  fzass4  9842  fzrev  9864  fz0fzelfz0  9904  fzocatel  9976  elfzomelpfzo  10008  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  qbtwnxr  10035  apbtwnz  10047  btwnzge0  10073  modqid  10122  modqcyc  10132  modqcyc2  10133  modqaddabs  10135  modqaddmod  10136  mulqaddmodid  10137  modqmuladd  10139  modqltm1p1mod  10149  modqsubmod  10155  modqsubmodmod  10156  modaddmodlo  10161  modqmulmod  10162  modqmulmodr  10163  modqsubdir  10166  addmodlteq  10171  iseqf1olemab  10262  iseqf1olemmo  10265  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  exp3val  10295  expcl2lemap  10305  expap0  10323  expnegzap  10327  expmul  10338  leexp1a  10348  expnbnd  10415  nn0opth2  10470  facndiv  10485  faclbnd  10487  bcval5  10509  bcpasc  10512  hashennnuni  10525  hashunlem  10550  hashunsng  10553  hashprg  10554  fiprsshashgt1  10563  hashxp  10572  fimaxq  10573  zfz1isolemiso  10582  zfz1isolem1  10583  seq3coll  10585  shftlem  10588  shftfvalg  10590  shftfval  10593  2shfti  10603  caucvgrelemrec  10751  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemcalc3  10788  resqrexlemcvg  10791  resqrexlemglsq  10794  resqrexlemga  10795  sqrtsq  10816  leabs  10846  absexpzap  10852  abslt  10860  absle  10861  abssubap0  10862  caubnd2  10889  icodiamlt  10952  maxleim  10977  maxabslemval  10980  maxleastlt  10987  rexico  10993  zmaxcl  10996  fimaxre2  10998  minmax  11001  xrmaxleim  11013  xrmaxiflemcl  11014  xrmaxifle  11015  xrmaxiflemlub  11017  xrmaxiflemval  11019  xrmaxleastlt  11025  xrmaxltsup  11027  xrmaxadd  11030  xrminmax  11034  xrbdtri  11045  climuni  11062  climshftlemg  11071  iserex  11108  climcau  11116  climrecvg1n  11117  climcvg1nlem  11118  sumeq2  11128  summodclem3  11149  zsumdc  11153  isumss  11160  fisumss  11161  sumsnf  11178  fsumconst  11223  modfsummod  11227  fsum00  11231  fsumabs  11234  fsumrelem  11240  fsumiun  11246  isumsplit  11260  divcnv  11266  geo2sum  11283  geoisumr  11287  cvgratz  11301  ntrivcvgap  11317  prodeq2  11326  prodmodclem2  11346  prodmodc  11347  tanaddap  11446  zdvdsdc  11514  dvds2ln  11526  dvdsle  11542  dvdsext  11553  divalglemeunn  11618  divalglemex  11619  divalglemeuneg  11620  zsupcllemstep  11638  dvdsbnd  11645  gcdsupex  11646  gcdsupcl  11647  dvdslegcd  11653  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlemzz  11690  bezoutlembz  11692  bezoutlembi  11693  bezoutlemle  11696  dfgcd3  11698  bezout  11699  dfgcd2  11702  dvdsmulgcd  11713  bezoutr  11720  lcmval  11744  lcmcllem  11748  lcmneg  11755  ncoprmgcdne1b  11770  isprm2lem  11797  prmind2  11801  dvdsnprmd  11806  prmdvdsexp  11826  sqrt2irr  11840  oddpwdclemxy  11847  oddpwdclemdc  11851  nonsq  11885  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  ennnfonelemfun  11930  ennnfonelemf1  11931  ennnfonelemim  11937  exmidunben  11939  ctiunctlemfo  11952  isstruct2r  11970  opnssneib  12325  restbasg  12337  restopn2  12352  iscnp4  12387  cnss2  12396  cnconst2  12402  cnptopresti  12407  cnptoprest2  12409  neitx  12437  uptx  12443  txrest  12445  txdis1cn  12447  xmetres2  12548  xblss2ps  12573  blhalf  12577  blssps  12596  blss  12597  blssexps  12598  blssex  12599  blin2  12601  metequiv2  12665  bdmetval  12669  metcnp3  12680  metcnp  12681  metcn  12683  metcnpi  12684  metcnpi2  12685  txmetcnp  12687  txmetcn  12688  qtopbas  12691  tgqioo  12716  fsumcncntop  12725  elcncf2  12730  mulcncflem  12759  mulcncf  12760  suplociccreex  12771  limcdifap  12800  cnplimcim  12805  cnplimccntop  12808  limccnpcntop  12813  dvcj  12842  dveflem  12855  sin0pilem1  12862  ptolemy  12905  coseq0q4123  12915  coseq0negpitopi  12917  cos02pilt1  12932  pwle2  13193  pwf1oexmid  13194  subctctexmid  13196  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfall  13204  nninfsellemeq  13210  nninfsellemqall  13211  sbthom  13221  refeq  13223  isomninnlem  13225  trilpolemeq1  13233  trilpolemlt1  13234