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 728	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  4929  f1prex  7320  fpr3g  8326  fprresex  8351  wfrlem17OLD  8381  nnaordex2  8695  naddssim  8741  eroveu  8870  undomOLD  9126  mapdom2  9214  domunfican  9389  fofinf1o  9400  finsschain  9429  wemaplem3  9617  oemapvali  9753  iunfictbso  10183  enfin2i  10390  fin1a2s  10483  ttukeylem6  10583  distrlem4pr  11095  mulcmpblnr  11140  prsrlem1  11141  dedekind  11453  divdivdiv  11995  divmuleq  11999  divsubdiv  12010  lediv12a  12188  xralrple  13267  ssfzo12bi  13811  seqcaopr  14090  leexp2r  14224  hashbclem  14501  wrd2ind  14771  rtrclreclem3  15109  rtrclreclem4  15110  relexpindlem  15112  rtrclind  15114  rlimresb  15611  summo  15765  fsum2dlem  15818  prodmo  15984  fprod2dlem  16028  bezoutlem3  16588  bezoutlem4  16589  ncoprmgcdne1b  16697  qredeu  16705  coprmproddvdslem  16709  prmdvdsncoprmbd  16774  pcqmul  16900  pcadd  16936  pockthg  16953  prmreclem2  16964  vdwlem10  17037  ramub1lem2  17074  prmgaplem6  17103  prmgaplem7  17104  cshwsdisj  17146  mreexexlem4d  17705  mreexdomd  17707  issubc3  17913  cofucl  17952  setcmon  18154  setcepi  18155  drsdirfi  18375  poslubmo  18481  posglbmo  18482  grprida  18713  rabsubmgmd  18742  issubmd  18841  mndind  18863  ghmpreima  19278  gaorber  19348  psgnunilem4  19539  psgneu  19548  odcau  19646  pgpssslw  19656  fislw  19667  lsmsubm  19695  efgsfo  19781  gsum2d2  20016  pgpfac1lem5  20123  pgpfac1  20124  pgpfaclem2  20126  pgpfaclem3  20127  unitgrp  20409  lmodprop2d  20944  lsspropd  21039  lbsextlem4  21186  assapropd  21915  evlslem1  22129  mdetunilem8  22646  mdetuni0  22648  mdetmul  22650  neiint  23133  restbas  23187  iscnp4  23292  cnpco  23296  nrmsep  23386  regsep2  23405  ordthauslem  23412  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  2ndcdisj  23485  2ndcomap  23487  dis2ndc  23489  nlly2i  23505  islly2  23513  hausllycmp  23523  lly1stc  23525  comppfsc  23561  ptbasin  23606  txcls  23633  ptcnp  23651  txlly  23665  txnlly  23666  txtube  23669  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  basqtop  23740  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  reghmph  23822  nrmhmph  23823  opnfbas  23871  rnelfmlem  23981  fmufil  23988  fclscf  24054  fclsfnflim  24056  flimfnfcls  24057  uffclsflim  24060  cnpfcfi  24069  cnpfcf  24070  alexsubALTlem2  24077  alexsubALTlem4  24079  tgpconncompeqg  24141  ghmcnp  24144  qustgplem  24150  tsmsxp  24184  blssps  24455  blss  24456  blcld  24539  metequiv2  24544  met2ndci  24556  prdsxmslem2  24563  txmetcnp  24581  nlmvscnlem1  24728  xrge0tsms  24875  ipcnlem1  25298  iscmet3  25346  metsscmetcld  25368  minveclem3  25482  pmltpc  25504  ovolscalem2  25568  ovolicc2lem5  25575  ovolicc2  25576  nulmbl2  25590  ioombl1  25616  uniioombllem6  25642  uniioombl  25643  vitalilem3  25664  i1faddlem  25747  mbfmullem  25780  itg2split  25804  lhop2  26074  dvfsumrlim  26092  itgsubst  26110  plydivex  26357  plyexmo  26373  ulmbdd  26459  cxploglim  27039  dchrptlem2  27327  lgsquad2lem2  27447  2sqlem5  27484  dchrvmasumif  27565  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem3  27581  dchrisum0  27582  dchrmusum  27586  dchrvmasum  27587  pntibndlem3  27654  pntlemp  27672  ostth3  27700  nosupbday  27768  nosupbnd1lem1  27771  nosupbnd2  27779  noinfno  27781  noinfbday  27783  noinfbnd1lem1  27786  noinfbnd2  27794  conway  27862  madebdaylemlrcut  27955  mulsproplem9  28168  mulsproplem13  28172  mulsproplem14  28173  mulsuniflem  28193  uzsind  28409  readdscl  28449  legtrid  28617  hlcgreu  28644  mirreu3  28680  midexlem  28718  opphllem  28761  mideulem  28762  opphllem1  28773  oppperpex  28779  lnperpex  28829  trgcopy  28830  iscgra1  28836  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  acopyeu  28860  ax5seglem9  28970  ax5seg  28971  axcontlem8  29004  axcontlem12  29008  clwwlknonwwlknonb  30138  2pthfrgr  30316  frgrnbnb  30325  ablo4  30582  smcnlem  30729  pjhthmo  31334  mdslmd1lem1  32357  xrge0tsmsd  33041  locfinref  33787  xpinpreima2  33853  qqhval2  33928  dya2iocnrect  34246  orvcgteel  34432  orvclteel  34437  derangenlem  35139  cnpconn  35198  txpconn  35200  connpconn  35203  pconnpi1  35205  iccllysconn  35218  rellysconn  35219  cvmcov2  35243  cvmliftmolem2  35250  cvmliftmo  35252  cvmliftlem15  35266  cvmliftpht  35286  cvmlift3lem2  35288  cgrextend  35972  btwnouttr2  35986  cgrsub  36009  cgrxfr  36019  btwnxfr  36020  colineardim1  36025  btwnconn1lem6  36056  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  seglecgr12im  36074  segleantisym  36079  outsideofeq  36094  outsidele  36096  lineunray  36111  linethru  36117  fnessref  36323  neibastop2lem  36326  neibastop2  36327  weiunpo  36431  unblimceq0lem  36472  knoppndvlem22  36499  bj-finsumval0  37251  isbasisrelowllem1  37321  isbasisrelowllem2  37322  mblfinlem3  37619  cnambfre  37628  areacirclem5  37672  istotbnd3  37731  sstotbnd  37735  crngm4  37963  cvlcvr1  39295  4atlem12  39569  paddasslem10  39786  paddasslem12  39788  paddasslem13  39789  lhpexle3lem  39968  cdlemd4  40158  cdleme0cq  40172  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme32d  40401  cdleme32f  40403  cdleme40m  40424  cdleme40n  40425  cdleme42keg  40443  cdleme42mgN  40445  cdleme50trn2  40508  cdleme50trn3  40510  cdlemm10N  41075  dihvalcqpre  41192  dihopelvalcpre  41205  dihmeetlem1N  41247  dihjat1lem  41385  mapd0  41622  mapdh9a  41746  fsuppssind  42548  nna4b4nsq  42615  diophin  42728  pellexlem3  42787  pellexlem5  42789  pellex  42791  pell14qrmulcl  42819  jm2.19lem3  42948  jm2.25  42956  jm2.27b  42963  lmhmfgsplit  43043  hbtlem2  43081  hbtlem5  43085  gsumws3  44158  gsumws4  44159  mnuprdlem4  44244  fnchoice  44929  stoweidlem17  45938  stoweidlem53  45974  stoweidlem61  45982  qndenserrnbllem  46215  bgoldbtbnd  47683  lindslinindsimp1  48186  prsthinc  48721