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  4848  f1prex  7239  fpr3g  8235  fprresex  8260  nnaordex2  8575  naddssim  8621  eroveu  8759  mapdom2  9086  domunfican  9232  fofinf1o  9242  finsschain  9269  wemaplem3  9463  oemapvali  9605  iunfictbso  10036  enfin2i  10243  fin1a2s  10336  ttukeylem6  10436  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  dedekind  11309  divdivdiv  11856  divmuleq  11860  divsubdiv  11871  lediv12a  12049  xralrple  13157  ssfzo12bi  13716  seqcaopr  14001  leexp2r  14136  hashbclem  14414  wrd2ind  14685  rtrclreclem3  15022  rtrclreclem4  15023  relexpindlem  15025  rtrclind  15027  rlimresb  15527  summo  15679  fsum2dlem  15732  prodmo  15901  fprod2dlem  15945  bezoutlem3  16510  bezoutlem4  16511  ncoprmgcdne1b  16619  qredeu  16627  coprmproddvdslem  16631  prmdvdsncoprmbd  16697  pcqmul  16824  pcadd  16860  pockthg  16877  prmreclem2  16888  vdwlem10  16961  ramub1lem2  16998  prmgaplem6  17027  prmgaplem7  17028  cshwsdisj  17069  mreexexlem4d  17613  mreexdomd  17615  issubc3  17816  cofucl  17855  setcmon  18054  setcepi  18055  drsdirfi  18271  poslubmo  18375  posglbmo  18376  grprida  18643  rabsubmgmd  18672  issubmd  18774  mndind  18796  ghmpreima  19213  gaorber  19283  psgnunilem4  19472  psgneu  19481  odcau  19579  pgpssslw  19589  fislw  19600  lsmsubm  19628  efgsfo  19714  gsum2d2  19949  pgpfac1lem5  20056  pgpfac1  20057  pgpfaclem2  20059  pgpfaclem3  20060  unitgrp  20363  lmodprop2d  20919  lsspropd  21012  lbsextlem4  21159  assapropd  21851  evlslem1  22060  mdetunilem8  22584  mdetuni0  22586  mdetmul  22588  neiint  23069  restbas  23123  iscnp4  23228  cnpco  23232  nrmsep  23322  regsep2  23341  ordthauslem  23348  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  2ndcdisj  23421  2ndcomap  23423  dis2ndc  23425  nlly2i  23441  islly2  23449  hausllycmp  23459  lly1stc  23461  comppfsc  23497  ptbasin  23542  txcls  23569  ptcnp  23587  txlly  23601  txnlly  23602  txtube  23605  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  basqtop  23676  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  reghmph  23758  nrmhmph  23759  opnfbas  23807  rnelfmlem  23917  fmufil  23924  fclscf  23990  fclsfnflim  23992  flimfnfcls  23993  uffclsflim  23996  cnpfcfi  24005  cnpfcf  24006  alexsubALTlem2  24013  alexsubALTlem4  24015  tgpconncompeqg  24077  ghmcnp  24080  qustgplem  24086  tsmsxp  24120  blssps  24389  blss  24390  blcld  24470  metequiv2  24475  met2ndci  24487  prdsxmslem2  24494  txmetcnp  24512  nlmvscnlem1  24651  xrge0tsms  24800  ipcnlem1  25212  iscmet3  25260  metsscmetcld  25282  minveclem3  25396  pmltpc  25417  ovolscalem2  25481  ovolicc2lem5  25488  ovolicc2  25489  nulmbl2  25503  ioombl1  25529  uniioombllem6  25555  uniioombl  25556  vitalilem3  25577  i1faddlem  25660  mbfmullem  25692  itg2split  25716  lhop2  25982  dvfsumrlim  25998  itgsubst  26016  plydivex  26263  plyexmo  26279  ulmbdd  26363  cxploglim  26941  dchrptlem2  27228  lgsquad2lem2  27348  2sqlem5  27385  dchrvmasumif  27466  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  dchrmusum  27487  dchrvmasum  27488  pntibndlem3  27555  pntlemp  27573  ostth3  27601  nosupbday  27669  nosupbnd1lem1  27672  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1lem1  27687  noinfbnd2  27695  conway  27771  madebdaylemlrcut  27891  mulsproplem9  28116  mulsproplem13  28120  mulsproplem14  28121  mulsuniflem  28141  uzsind  28397  bdayfinbndlem1  28459  readdscl  28491  legtrid  28659  hlcgreu  28686  mirreu3  28722  midexlem  28760  opphllem  28803  mideulem  28804  opphllem1  28815  oppperpex  28821  lnperpex  28871  trgcopy  28872  iscgra1  28878  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  acopyeu  28902  ax5seglem9  29006  ax5seg  29007  axcontlem8  29040  axcontlem12  29044  clwwlknonwwlknonb  30176  2pthfrgr  30354  frgrnbnb  30363  ablo4  30621  smcnlem  30768  pjhthmo  31373  mdslmd1lem1  32396  xrge0tsmsd  33134  locfinref  33985  xpinpreima2  34051  qqhval2  34126  dya2iocnrect  34425  orvcgteel  34612  orvclteel  34617  derangenlem  35353  cnpconn  35412  txpconn  35414  connpconn  35417  pconnpi1  35419  iccllysconn  35432  rellysconn  35433  cvmcov2  35457  cvmliftmolem2  35464  cvmliftmo  35466  cvmliftlem15  35480  cvmliftpht  35500  cvmlift3lem2  35502  cgrextend  36190  btwnouttr2  36204  cgrsub  36227  cgrxfr  36237  btwnxfr  36238  colineardim1  36243  btwnconn1lem6  36274  btwnconn1lem13  36281  btwnconn1lem14  36282  btwnconn3  36285  seglecgr12im  36292  segleantisym  36297  outsideofeq  36312  outsidele  36314  lineunray  36329  linethru  36335  fnessref  36539  neibastop2lem  36542  neibastop2  36543  weiunpo  36647  unblimceq0lem  36766  knoppndvlem22  36793  bj-finsumval0  37599  isbasisrelowllem1  37671  isbasisrelowllem2  37672  mblfinlem3  37980  cnambfre  37989  areacirclem5  38033  istotbnd3  38092  sstotbnd  38096  crngm4  38324  cvlcvr1  39785  4atlem12  40058  paddasslem10  40275  paddasslem12  40277  paddasslem13  40278  lhpexle3lem  40457  cdlemd4  40647  cdleme0cq  40661  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme32d  40890  cdleme32f  40892  cdleme40m  40913  cdleme40n  40914  cdleme42keg  40932  cdleme42mgN  40934  cdleme50trn2  40997  cdleme50trn3  40999  cdlemm10N  41564  dihvalcqpre  41681  dihopelvalcpre  41694  dihmeetlem1N  41736  dihjat1lem  41874  mapd0  42111  mapdh9a  42235  fsuppssind  43026  nna4b4nsq  43093  diophin  43204  pellexlem3  43259  pellexlem5  43261  pellex  43263  pell14qrmulcl  43291  jm2.19lem3  43419  jm2.25  43427  jm2.27b  43434  lmhmfgsplit  43514  hbtlem2  43552  hbtlem5  43556  gsumws3  44623  gsumws4  44624  mnuprdlem4  44702  fnchoice  45460  stoweidlem17  46445  stoweidlem53  46481  stoweidlem61  46489  qndenserrnbllem  46722  bgoldbtbnd  48285  cycldlenngric  48404  isubgr3stgrlem6  48447  lindslinindsimp1  48933  brab2dd  49303  prsthinc  49939