Theorem simprrl 792

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 487	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 741	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  prproe  4866  f1prex  7272  fpr3g  8270  fprresex  8295  nnaordex2  8613  naddssim  8660  eroveu  8798  mapdom2  9124  domunfican  9269  fofinf1o  9277  finsschain  9304  wemaplem3  9498  oemapvali  9641  iunfictbso  10086  enfin2i  10293  fin1a2s  10386  ttukeylem6  10486  distrlem4pr  10999  mulcmpblnr  11044  prsrlem1  11045  dedekind  11361  divdivdiv  11907  divmuleq  11911  divsubdiv  11922  lediv12a  12099  xralrple  13222  ssfzo12bi  13781  seqcaopr  14066  leexp2r  14201  hashbclem  14479  wrd2ind  14750  rtrclreclem3  15087  rtrclreclem4  15088  relexpindlem  15090  rtrclind  15092  rlimresb  15606  summo  15758  fsum2dlem  15811  prodmo  15980  fprod2dlem  16024  bezoutlem3  16589  bezoutlem4  16590  ncoprmgcdne1b  16698  qredeu  16706  coprmproddvdslem  16710  prmdvdsncoprmbd  16776  pcqmul  16903  pcadd  16939  pockthg  16956  prmreclem2  16967  vdwlem10  17040  ramub1lem2  17077  prmgaplem6  17106  prmgaplem7  17107  cshwsdisj  17148  mreexexlem4d  17693  mreexdomd  17695  issubc3  17896  cofucl  17935  setcmon  18134  setcepi  18135  drsdirfi  18351  poslubmo  18455  posglbmo  18456  grprida  18723  rabsubmgmd  18752  issubmd  18854  mndind  18877  ghmpreima  19299  gaorber  19369  psgnunilem4  19558  psgneu  19567  odcau  19665  pgpssslw  19675  fislw  19686  lsmsubm  19714  efgsfo  19800  gsum2d2  20035  pgpfac1lem5  20142  pgpfac1  20143  pgpfaclem2  20145  pgpfaclem3  20146  unitgrp  20456  lmodprop2d  21014  lsspropd  21107  lbsextlem4  21254  assapropd  21981  evlslem1  22193  mdetunilem8  22737  mdetuni0  22739  mdetmul  22741  neiint  23222  restbas  23276  iscnp4  23381  cnpco  23385  nrmsep  23475  regsep2  23494  ordthauslem  23501  1stcfb  23563  1stcrest  23571  2ndcctbss  23573  2ndcdisj  23574  2ndcomap  23576  dis2ndc  23578  nlly2i  23594  islly2  23602  hausllycmp  23612  lly1stc  23614  comppfsc  23650  ptbasin  23695  txcls  23722  ptcnp  23740  txlly  23754  txnlly  23755  txtube  23758  txcmplem1  23759  txcmplem2  23760  xkococnlem  23777  basqtop  23829  regr1lem  23857  kqreglem1  23859  kqreglem2  23860  kqnrmlem1  23861  kqnrmlem2  23862  reghmph  23911  nrmhmph  23912  opnfbas  23960  rnelfmlem  24070  fmufil  24077  fclscf  24143  fclsfnflim  24145  flimfnfcls  24146  uffclsflim  24149  cnpfcfi  24158  cnpfcf  24159  alexsubALTlem2  24166  alexsubALTlem4  24168  tgpconncompeqg  24230  ghmcnp  24233  qustgplem  24239  tsmsxp  24273  blssps  24542  blss  24543  blcld  24623  metequiv2  24628  met2ndci  24640  prdsxmslem2  24647  txmetcnp  24665  nlmvscnlem1  24804  xrge0tsms  24953  ipcnlem1  25365  iscmet3  25413  metsscmetcld  25435  minveclem3  25549  pmltpc  25570  ovolscalem2  25634  ovolicc2lem5  25641  ovolicc2  25642  nulmbl2  25656  ioombl1  25682  uniioombllem6  25708  uniioombl  25709  vitalilem3  25730  i1faddlem  25813  mbfmullem  25845  itg2split  25869  lhop2  26135  dvfsumrlim  26151  itgsubst  26169  plydivex  26419  plyexmo  26435  ulmbdd  26519  cxploglim  27100  dchrptlem2  27387  lgsquad2lem2  27507  2sqlem5  27544  dchrvmasumif  27625  rpvmasum2  27634  dchrisum0re  27635  dchrisum0lem3  27641  dchrisum0  27642  dchrmusum  27646  dchrvmasum  27647  pntibndlem3  27714  pntlemp  27732  ostth3  27760  nosupbday  27827  nosupbnd1lem1  27830  nosupbnd2  27838  noinfno  27840  noinfbday  27842  noinfbnd1lem1  27845  noinfbnd2  27853  conway  27930  madebdaylemlrcut  28050  mulsproplem9  28275  mulsproplem13  28279  mulsproplem14  28280  mulsuniflem  28300  uzsind  28556  bdayfinbndlem1  28618  readdscl  28650  legtrid  28818  hlcgreu  28845  mirreu3  28885  midexlem  28923  opphllem  28966  mideulem  28967  opphllem1  28978  oppperpex  28984  lnperpex  29055  trgcopy  29056  iscgra1  29062  cgraswap  29072  cgracom  29074  cgratr  29075  flatcgra  29076  acopyeu  29086  ax5seglem9  29196  ax5seg  29197  axcontlem8  29230  axcontlem12  29234  clwwlknonwwlknonb  30366  2pthfrgr  30544  frgrnbnb  30553  ablo4  30811  smcnlem  30958  pjhthmo  31563  mdslmd1lem1  32586  xrge0tsmsd  33306  locfinref  34148  xpinpreima2  34214  qqhval2  34289  dya2iocnrect  34588  orvcgteel  34775  orvclteel  34780  derangenlem  35534  cnpconn  35593  txpconn  35595  connpconn  35598  pconnpi1  35600  iccllysconn  35613  rellysconn  35614  cvmcov2  35638  cvmliftmolem2  35645  cvmliftmo  35647  cvmliftlem15  35661  cvmliftpht  35681  cvmlift3lem2  35683  cgrextend  36371  btwnouttr2  36385  cgrsub  36408  cgrxfr  36418  btwnxfr  36419  colineardim1  36424  btwnconn1lem6  36455  btwnconn1lem13  36462  btwnconn1lem14  36463  btwnconn3  36466  seglecgr12im  36473  segleantisym  36478  outsideofeq  36493  outsidele  36495  lineunray  36510  linethru  36516  fnessref  36730  neibastop2lem  36733  neibastop2  36734  weiunpo  36838  unblimceq0lem  36957  knoppndvlem22  36984  bj-finsumval0  37789  isbasisrelowllem1  37861  isbasisrelowllem2  37862  mblfinlem3  38170  cnambfre  38179  areacirclem5  38223  istotbnd3  38282  sstotbnd  38286  crngm4  38514  cvlcvr1  39975  4atlem12  40248  paddasslem10  40465  paddasslem12  40467  paddasslem13  40468  lhpexle3lem  40647  cdlemd4  40837  cdleme0cq  40851  cdlemefs32sn1aw  41050  cdleme43fsv1snlem  41056  cdleme32d  41080  cdleme32f  41082  cdleme40m  41103  cdleme40n  41104  cdleme42keg  41122  cdleme42mgN  41124  cdleme50trn2  41187  cdleme50trn3  41189  cdlemm10N  41754  dihvalcqpre  41871  dihopelvalcpre  41884  dihmeetlem1N  41926  dihjat1lem  42064  mapd0  42301  mapdh9a  42425  fsuppssind  43187  nna4b4nsq  43254  diophin  43365  pellexlem3  43420  pellexlem5  43422  pellex  43424  pell14qrmulcl  43452  jm2.19lem3  43580  jm2.25  43588  jm2.27b  43595  lmhmfgsplit  43675  hbtlem2  43713  hbtlem5  43717  gsumws3  44784  gsumws4  44785  mnuprdlem4  44849  fnchoice  45607  stoweidlem17  46589  stoweidlem53  46625  stoweidlem61  46633  qndenserrnbllem  46866  bgoldbtbnd  48429  cycldlenngric  48548  isubgr3stgrlem6  48591  lindslinindsimp1  49088  brab2dd  49457  prsthinc  50093