Theorem simprrl 780

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 729	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  4872  f1prex  7262  fpr3g  8267  fprresex  8292  nnaordex2  8606  naddssim  8652  eroveu  8788  undomOLD  9034  mapdom2  9118  domunfican  9279  fofinf1o  9290  finsschain  9317  wemaplem3  9508  oemapvali  9644  iunfictbso  10074  enfin2i  10281  fin1a2s  10374  ttukeylem6  10474  distrlem4pr  10986  mulcmpblnr  11031  prsrlem1  11032  dedekind  11344  divdivdiv  11890  divmuleq  11894  divsubdiv  11905  lediv12a  12083  xralrple  13172  ssfzo12bi  13729  seqcaopr  14011  leexp2r  14146  hashbclem  14424  wrd2ind  14695  rtrclreclem3  15033  rtrclreclem4  15034  relexpindlem  15036  rtrclind  15038  rlimresb  15538  summo  15690  fsum2dlem  15743  prodmo  15909  fprod2dlem  15953  bezoutlem3  16518  bezoutlem4  16519  ncoprmgcdne1b  16627  qredeu  16635  coprmproddvdslem  16639  prmdvdsncoprmbd  16704  pcqmul  16831  pcadd  16867  pockthg  16884  prmreclem2  16895  vdwlem10  16968  ramub1lem2  17005  prmgaplem6  17034  prmgaplem7  17035  cshwsdisj  17076  mreexexlem4d  17615  mreexdomd  17617  issubc3  17818  cofucl  17857  setcmon  18056  setcepi  18057  drsdirfi  18273  poslubmo  18377  posglbmo  18378  grprida  18609  rabsubmgmd  18638  issubmd  18740  mndind  18762  ghmpreima  19177  gaorber  19247  psgnunilem4  19434  psgneu  19443  odcau  19541  pgpssslw  19551  fislw  19562  lsmsubm  19590  efgsfo  19676  gsum2d2  19911  pgpfac1lem5  20018  pgpfac1  20019  pgpfaclem2  20021  pgpfaclem3  20022  unitgrp  20299  lmodprop2d  20837  lsspropd  20931  lbsextlem4  21078  assapropd  21788  evlslem1  21996  mdetunilem8  22513  mdetuni0  22515  mdetmul  22517  neiint  22998  restbas  23052  iscnp4  23157  cnpco  23161  nrmsep  23251  regsep2  23270  ordthauslem  23277  1stcfb  23339  1stcrest  23347  2ndcctbss  23349  2ndcdisj  23350  2ndcomap  23352  dis2ndc  23354  nlly2i  23370  islly2  23378  hausllycmp  23388  lly1stc  23390  comppfsc  23426  ptbasin  23471  txcls  23498  ptcnp  23516  txlly  23530  txnlly  23531  txtube  23534  txcmplem1  23535  txcmplem2  23536  xkococnlem  23553  basqtop  23605  regr1lem  23633  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  reghmph  23687  nrmhmph  23688  opnfbas  23736  rnelfmlem  23846  fmufil  23853  fclscf  23919  fclsfnflim  23921  flimfnfcls  23922  uffclsflim  23925  cnpfcfi  23934  cnpfcf  23935  alexsubALTlem2  23942  alexsubALTlem4  23944  tgpconncompeqg  24006  ghmcnp  24009  qustgplem  24015  tsmsxp  24049  blssps  24319  blss  24320  blcld  24400  metequiv2  24405  met2ndci  24417  prdsxmslem2  24424  txmetcnp  24442  nlmvscnlem1  24581  xrge0tsms  24730  ipcnlem1  25152  iscmet3  25200  metsscmetcld  25222  minveclem3  25336  pmltpc  25358  ovolscalem2  25422  ovolicc2lem5  25429  ovolicc2  25430  nulmbl2  25444  ioombl1  25470  uniioombllem6  25496  uniioombl  25497  vitalilem3  25518  i1faddlem  25601  mbfmullem  25633  itg2split  25657  lhop2  25927  dvfsumrlim  25945  itgsubst  25963  plydivex  26212  plyexmo  26228  ulmbdd  26314  cxploglim  26895  dchrptlem2  27183  lgsquad2lem2  27303  2sqlem5  27340  dchrvmasumif  27421  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem3  27437  dchrisum0  27438  dchrmusum  27442  dchrvmasum  27443  pntibndlem3  27510  pntlemp  27528  ostth3  27556  nosupbday  27624  nosupbnd1lem1  27627  nosupbnd2  27635  noinfno  27637  noinfbday  27639  noinfbnd1lem1  27642  noinfbnd2  27650  conway  27718  madebdaylemlrcut  27817  mulsproplem9  28034  mulsproplem13  28038  mulsproplem14  28039  mulsuniflem  28059  uzsind  28300  readdscl  28357  legtrid  28525  hlcgreu  28552  mirreu3  28588  midexlem  28626  opphllem  28669  mideulem  28670  opphllem1  28681  oppperpex  28687  lnperpex  28737  trgcopy  28738  iscgra1  28744  cgraswap  28754  cgracom  28756  cgratr  28757  flatcgra  28758  acopyeu  28768  ax5seglem9  28871  ax5seg  28872  axcontlem8  28905  axcontlem12  28909  clwwlknonwwlknonb  30042  2pthfrgr  30220  frgrnbnb  30229  ablo4  30486  smcnlem  30633  pjhthmo  31238  mdslmd1lem1  32261  xrge0tsmsd  33009  locfinref  33838  xpinpreima2  33904  qqhval2  33979  dya2iocnrect  34279  orvcgteel  34466  orvclteel  34471  derangenlem  35165  cnpconn  35224  txpconn  35226  connpconn  35229  pconnpi1  35231  iccllysconn  35244  rellysconn  35245  cvmcov2  35269  cvmliftmolem2  35276  cvmliftmo  35278  cvmliftlem15  35292  cvmliftpht  35312  cvmlift3lem2  35314  cgrextend  36003  btwnouttr2  36017  cgrsub  36040  cgrxfr  36050  btwnxfr  36051  colineardim1  36056  btwnconn1lem6  36087  btwnconn1lem13  36094  btwnconn1lem14  36095  btwnconn3  36098  seglecgr12im  36105  segleantisym  36110  outsideofeq  36125  outsidele  36127  lineunray  36142  linethru  36148  fnessref  36352  neibastop2lem  36355  neibastop2  36356  weiunpo  36460  unblimceq0lem  36501  knoppndvlem22  36528  bj-finsumval0  37280  isbasisrelowllem1  37350  isbasisrelowllem2  37351  mblfinlem3  37660  cnambfre  37669  areacirclem5  37713  istotbnd3  37772  sstotbnd  37776  crngm4  38004  cvlcvr1  39339  4atlem12  39613  paddasslem10  39830  paddasslem12  39832  paddasslem13  39833  lhpexle3lem  40012  cdlemd4  40202  cdleme0cq  40216  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme32d  40445  cdleme32f  40447  cdleme40m  40468  cdleme40n  40469  cdleme42keg  40487  cdleme42mgN  40489  cdleme50trn2  40552  cdleme50trn3  40554  cdlemm10N  41119  dihvalcqpre  41236  dihopelvalcpre  41249  dihmeetlem1N  41291  dihjat1lem  41429  mapd0  41666  mapdh9a  41790  fsuppssind  42588  nna4b4nsq  42655  diophin  42767  pellexlem3  42826  pellexlem5  42828  pellex  42830  pell14qrmulcl  42858  jm2.19lem3  42987  jm2.25  42995  jm2.27b  43002  lmhmfgsplit  43082  hbtlem2  43120  hbtlem5  43124  gsumws3  44192  gsumws4  44193  mnuprdlem4  44271  fnchoice  45030  stoweidlem17  46022  stoweidlem53  46058  stoweidlem61  46066  qndenserrnbllem  46299  bgoldbtbnd  47814  cycldlenngric  47932  isubgr3stgrlem6  47974  lindslinindsimp1  48450  brab2dd  48820  prsthinc  49457