Theorem simprrl 781

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4863  f1prex  7240  fpr3g  8237  fprresex  8262  nnaordex2  8577  naddssim  8623  eroveu  8761  mapdom2  9088  domunfican  9234  fofinf1o  9244  finsschain  9271  wemaplem3  9465  oemapvali  9605  iunfictbso  10036  enfin2i  10243  fin1a2s  10336  ttukeylem6  10436  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  dedekind  11308  divdivdiv  11854  divmuleq  11858  divsubdiv  11869  lediv12a  12047  xralrple  13132  ssfzo12bi  13689  seqcaopr  13974  leexp2r  14109  hashbclem  14387  wrd2ind  14658  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  rtrclind  15000  rlimresb  15500  summo  15652  fsum2dlem  15705  prodmo  15871  fprod2dlem  15915  bezoutlem3  16480  bezoutlem4  16481  ncoprmgcdne1b  16589  qredeu  16597  coprmproddvdslem  16601  prmdvdsncoprmbd  16666  pcqmul  16793  pcadd  16829  pockthg  16846  prmreclem2  16857  vdwlem10  16930  ramub1lem2  16967  prmgaplem6  16996  prmgaplem7  16997  cshwsdisj  17038  mreexexlem4d  17582  mreexdomd  17584  issubc3  17785  cofucl  17824  setcmon  18023  setcepi  18024  drsdirfi  18240  poslubmo  18344  posglbmo  18345  grprida  18612  rabsubmgmd  18641  issubmd  18743  mndind  18765  ghmpreima  19179  gaorber  19249  psgnunilem4  19438  psgneu  19447  odcau  19545  pgpssslw  19555  fislw  19566  lsmsubm  19594  efgsfo  19680  gsum2d2  19915  pgpfac1lem5  20022  pgpfac1  20023  pgpfaclem2  20025  pgpfaclem3  20026  unitgrp  20331  lmodprop2d  20887  lsspropd  20981  lbsextlem4  21128  assapropd  21839  evlslem1  22049  mdetunilem8  22575  mdetuni0  22577  mdetmul  22579  neiint  23060  restbas  23114  iscnp4  23219  cnpco  23223  nrmsep  23313  regsep2  23332  ordthauslem  23339  1stcfb  23401  1stcrest  23409  2ndcctbss  23411  2ndcdisj  23412  2ndcomap  23414  dis2ndc  23416  nlly2i  23432  islly2  23440  hausllycmp  23450  lly1stc  23452  comppfsc  23488  ptbasin  23533  txcls  23560  ptcnp  23578  txlly  23592  txnlly  23593  txtube  23596  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  basqtop  23667  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  reghmph  23749  nrmhmph  23750  opnfbas  23798  rnelfmlem  23908  fmufil  23915  fclscf  23981  fclsfnflim  23983  flimfnfcls  23984  uffclsflim  23987  cnpfcfi  23996  cnpfcf  23997  alexsubALTlem2  24004  alexsubALTlem4  24006  tgpconncompeqg  24068  ghmcnp  24071  qustgplem  24077  tsmsxp  24111  blssps  24380  blss  24381  blcld  24461  metequiv2  24466  met2ndci  24478  prdsxmslem2  24485  txmetcnp  24503  nlmvscnlem1  24642  xrge0tsms  24791  ipcnlem1  25213  iscmet3  25261  metsscmetcld  25283  minveclem3  25397  pmltpc  25419  ovolscalem2  25483  ovolicc2lem5  25490  ovolicc2  25491  nulmbl2  25505  ioombl1  25531  uniioombllem6  25557  uniioombl  25558  vitalilem3  25579  i1faddlem  25662  mbfmullem  25694  itg2split  25718  lhop2  25988  dvfsumrlim  26006  itgsubst  26024  plydivex  26273  plyexmo  26289  ulmbdd  26375  cxploglim  26956  dchrptlem2  27244  lgsquad2lem2  27364  2sqlem5  27401  dchrvmasumif  27482  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem3  27498  dchrisum0  27499  dchrmusum  27503  dchrvmasum  27504  pntibndlem3  27571  pntlemp  27589  ostth3  27617  nosupbday  27685  nosupbnd1lem1  27688  nosupbnd2  27696  noinfno  27698  noinfbday  27700  noinfbnd1lem1  27703  noinfbnd2  27711  conway  27787  madebdaylemlrcut  27907  mulsproplem9  28132  mulsproplem13  28136  mulsproplem14  28137  mulsuniflem  28157  uzsind  28413  bdayfinbndlem1  28475  readdscl  28507  legtrid  28675  hlcgreu  28702  mirreu3  28738  midexlem  28776  opphllem  28819  mideulem  28820  opphllem1  28831  oppperpex  28837  lnperpex  28887  trgcopy  28888  iscgra1  28894  cgraswap  28904  cgracom  28906  cgratr  28907  flatcgra  28908  acopyeu  28918  ax5seglem9  29022  ax5seg  29023  axcontlem8  29056  axcontlem12  29060  clwwlknonwwlknonb  30193  2pthfrgr  30371  frgrnbnb  30380  ablo4  30637  smcnlem  30784  pjhthmo  31389  mdslmd1lem1  32412  xrge0tsmsd  33166  locfinref  34018  xpinpreima2  34084  qqhval2  34159  dya2iocnrect  34458  orvcgteel  34645  orvclteel  34650  derangenlem  35384  cnpconn  35443  txpconn  35445  connpconn  35448  pconnpi1  35450  iccllysconn  35463  rellysconn  35464  cvmcov2  35488  cvmliftmolem2  35495  cvmliftmo  35497  cvmliftlem15  35511  cvmliftpht  35531  cvmlift3lem2  35533  cgrextend  36221  btwnouttr2  36235  cgrsub  36258  cgrxfr  36268  btwnxfr  36269  colineardim1  36274  btwnconn1lem6  36305  btwnconn1lem13  36312  btwnconn1lem14  36313  btwnconn3  36316  seglecgr12im  36323  segleantisym  36328  outsideofeq  36343  outsidele  36345  lineunray  36360  linethru  36366  fnessref  36570  neibastop2lem  36573  neibastop2  36574  weiunpo  36678  unblimceq0lem  36725  knoppndvlem22  36752  bj-finsumval0  37534  isbasisrelowllem1  37604  isbasisrelowllem2  37605  mblfinlem3  37904  cnambfre  37913  areacirclem5  37957  istotbnd3  38016  sstotbnd  38020  crngm4  38248  cvlcvr1  39709  4atlem12  39982  paddasslem10  40199  paddasslem12  40201  paddasslem13  40202  lhpexle3lem  40381  cdlemd4  40571  cdleme0cq  40585  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdleme32d  40814  cdleme32f  40816  cdleme40m  40837  cdleme40n  40838  cdleme42keg  40856  cdleme42mgN  40858  cdleme50trn2  40921  cdleme50trn3  40923  cdlemm10N  41488  dihvalcqpre  41605  dihopelvalcpre  41618  dihmeetlem1N  41660  dihjat1lem  41798  mapd0  42035  mapdh9a  42159  fsuppssind  42945  nna4b4nsq  43012  diophin  43123  pellexlem3  43182  pellexlem5  43184  pellex  43186  pell14qrmulcl  43214  jm2.19lem3  43342  jm2.25  43350  jm2.27b  43357  lmhmfgsplit  43437  hbtlem2  43475  hbtlem5  43479  gsumws3  44546  gsumws4  44547  mnuprdlem4  44625  fnchoice  45383  stoweidlem17  46369  stoweidlem53  46405  stoweidlem61  46413  qndenserrnbllem  46646  bgoldbtbnd  48163  cycldlenngric  48282  isubgr3stgrlem6  48325  lindslinindsimp1  48811  brab2dd  49181  prsthinc  49817