Theorem simprrl 779

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrl	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 481	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 727	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  prproe  4914  f1prex  7301  fpr3g  8305  fprresex  8330  wfrlem17OLD  8360  nnaordex2  8674  naddssim  8720  eroveu  8846  undomOLD  9102  mapdom2  9190  domunfican  9365  fofinf1o  9376  finsschain  9405  wemaplem3  9593  oemapvali  9729  iunfictbso  10159  enfin2i  10366  fin1a2s  10459  ttukeylem6  10559  distrlem4pr  11071  mulcmpblnr  11116  prsrlem1  11117  dedekind  11429  divdivdiv  11971  divmuleq  11975  divsubdiv  11986  lediv12a  12164  xralrple  13243  ssfzo12bi  13786  seqcaopr  14065  leexp2r  14199  hashbclem  14476  wrd2ind  14745  rtrclreclem3  15079  rtrclreclem4  15080  relexpindlem  15082  rtrclind  15084  rlimresb  15581  summo  15735  fsum2dlem  15788  prodmo  15952  fprod2dlem  15996  bezoutlem3  16556  bezoutlem4  16557  ncoprmgcdne1b  16665  qredeu  16673  coprmproddvdslem  16677  prmdvdsncoprmbd  16743  pcqmul  16869  pcadd  16905  pockthg  16922  prmreclem2  16933  vdwlem10  17006  ramub1lem2  17043  prmgaplem6  17072  prmgaplem7  17073  cshwsdisj  17115  mreexexlem4d  17674  mreexdomd  17676  issubc3  17882  cofucl  17921  setcmon  18123  setcepi  18124  drsdirfi  18344  poslubmo  18450  posglbmo  18451  grprida  18682  rabsubmgmd  18711  issubmd  18810  mndind  18832  ghmpreima  19247  gaorber  19317  psgnunilem4  19508  psgneu  19517  odcau  19615  pgpssslw  19625  fislw  19636  lsmsubm  19664  efgsfo  19750  gsum2d2  19985  pgpfac1lem5  20092  pgpfac1  20093  pgpfaclem2  20095  pgpfaclem3  20096  unitgrp  20378  lmodprop2d  20913  lsspropd  21008  lbsextlem4  21155  assapropd  21883  evlslem1  22097  mdetunilem8  22613  mdetuni0  22615  mdetmul  22617  neiint  23100  restbas  23154  iscnp4  23259  cnpco  23263  nrmsep  23353  regsep2  23372  ordthauslem  23379  1stcfb  23441  1stcrest  23449  2ndcctbss  23451  2ndcdisj  23452  2ndcomap  23454  dis2ndc  23456  nlly2i  23472  islly2  23480  hausllycmp  23490  lly1stc  23492  comppfsc  23528  ptbasin  23573  txcls  23600  ptcnp  23618  txlly  23632  txnlly  23633  txtube  23636  txcmplem1  23637  txcmplem2  23638  xkococnlem  23655  basqtop  23707  regr1lem  23735  kqreglem1  23737  kqreglem2  23738  kqnrmlem1  23739  kqnrmlem2  23740  reghmph  23789  nrmhmph  23790  opnfbas  23838  rnelfmlem  23948  fmufil  23955  fclscf  24021  fclsfnflim  24023  flimfnfcls  24024  uffclsflim  24027  cnpfcfi  24036  cnpfcf  24037  alexsubALTlem2  24044  alexsubALTlem4  24046  tgpconncompeqg  24108  ghmcnp  24111  qustgplem  24117  tsmsxp  24151  blssps  24422  blss  24423  blcld  24506  metequiv2  24511  met2ndci  24523  prdsxmslem2  24530  txmetcnp  24548  nlmvscnlem1  24695  xrge0tsms  24842  ipcnlem1  25265  iscmet3  25313  metsscmetcld  25335  minveclem3  25449  pmltpc  25471  ovolscalem2  25535  ovolicc2lem5  25542  ovolicc2  25543  nulmbl2  25557  ioombl1  25583  uniioombllem6  25609  uniioombl  25610  vitalilem3  25631  i1faddlem  25714  mbfmullem  25747  itg2split  25771  lhop2  26040  dvfsumrlim  26058  itgsubst  26076  plydivex  26323  plyexmo  26339  ulmbdd  26425  cxploglim  27004  dchrptlem2  27292  lgsquad2lem2  27412  2sqlem5  27449  dchrvmasumif  27530  rpvmasum2  27539  dchrisum0re  27540  dchrisum0lem3  27546  dchrisum0  27547  dchrmusum  27551  dchrvmasum  27552  pntibndlem3  27619  pntlemp  27637  ostth3  27665  nosupbday  27733  nosupbnd1lem1  27736  nosupbnd2  27744  noinfno  27746  noinfbday  27748  noinfbnd1lem1  27751  noinfbnd2  27759  conway  27827  madebdaylemlrcut  27920  mulsproplem9  28125  mulsproplem13  28129  mulsproplem14  28130  mulsuniflem  28150  uzsind  28359  readdscl  28393  legtrid  28561  hlcgreu  28588  mirreu3  28624  midexlem  28662  opphllem  28705  mideulem  28706  opphllem1  28717  oppperpex  28723  lnperpex  28773  trgcopy  28774  iscgra1  28780  cgraswap  28790  cgracom  28792  cgratr  28793  flatcgra  28794  acopyeu  28804  ax5seglem9  28914  ax5seg  28915  axcontlem8  28948  axcontlem12  28952  clwwlknonwwlknonb  30082  2pthfrgr  30260  frgrnbnb  30269  ablo4  30526  smcnlem  30673  pjhthmo  31278  mdslmd1lem1  32301  xrge0tsmsd  32987  locfinref  33733  xpinpreima2  33799  qqhval2  33874  dya2iocnrect  34192  orvcgteel  34378  orvclteel  34383  derangenlem  35085  cnpconn  35144  txpconn  35146  connpconn  35149  pconnpi1  35151  iccllysconn  35164  rellysconn  35165  cvmcov2  35189  cvmliftmolem2  35196  cvmliftmo  35198  cvmliftlem15  35212  cvmliftpht  35232  cvmlift3lem2  35234  cgrextend  35918  btwnouttr2  35932  cgrsub  35955  cgrxfr  35965  btwnxfr  35966  colineardim1  35971  btwnconn1lem6  36002  btwnconn1lem13  36009  btwnconn1lem14  36010  btwnconn3  36013  seglecgr12im  36020  segleantisym  36025  outsideofeq  36040  outsidele  36042  lineunray  36057  linethru  36063  fnessref  36156  neibastop2lem  36159  neibastop2  36160  unblimceq0lem  36296  knoppndvlem22  36323  bj-finsumval0  37078  isbasisrelowllem1  37148  isbasisrelowllem2  37149  mblfinlem3  37446  cnambfre  37455  areacirclem5  37499  istotbnd3  37558  sstotbnd  37562  crngm4  37790  cvlcvr1  39123  4atlem12  39397  paddasslem10  39614  paddasslem12  39616  paddasslem13  39617  lhpexle3lem  39796  cdlemd4  39986  cdleme0cq  40000  cdlemefs32sn1aw  40199  cdleme43fsv1snlem  40205  cdleme32d  40229  cdleme32f  40231  cdleme40m  40252  cdleme40n  40253  cdleme42keg  40271  cdleme42mgN  40273  cdleme50trn2  40336  cdleme50trn3  40338  cdlemm10N  40903  dihvalcqpre  41020  dihopelvalcpre  41033  dihmeetlem1N  41075  dihjat1lem  41213  mapd0  41450  mapdh9a  41574  fsuppssind  42360  nna4b4nsq  42427  diophin  42544  pellexlem3  42603  pellexlem5  42605  pellex  42607  pell14qrmulcl  42635  jm2.19lem3  42764  jm2.25  42772  jm2.27b  42779  lmhmfgsplit  42862  hbtlem2  42900  hbtlem5  42904  gsumws3  43978  gsumws4  43979  mnuprdlem4  44064  fnchoice  44743  stoweidlem17  45752  stoweidlem53  45788  stoweidlem61  45796  qndenserrnbllem  46029  bgoldbtbnd  47495  lindslinindsimp1  47965  prsthinc  48500