Theorem simprrl 779

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  prproe  4906  f1prex  7284  fpr3g  8272  fprresex  8297  wfrlem17OLD  8327  naddssim  8686  eroveu  8808  undomOLD  9062  mapdom2  9150  domunfican  9322  fofinf1o  9329  finsschain  9361  wemaplem3  9545  oemapvali  9681  iunfictbso  10111  enfin2i  10318  fin1a2s  10411  ttukeylem6  10511  distrlem4pr  11023  mulcmpblnr  11068  prsrlem1  11069  dedekind  11381  divdivdiv  11919  divmuleq  11923  divsubdiv  11934  lediv12a  12111  xralrple  13188  ssfzo12bi  13731  seqcaopr  14009  leexp2r  14143  hashbclem  14415  wrd2ind  14677  rtrclreclem3  15011  rtrclreclem4  15012  relexpindlem  15014  rtrclind  15016  rlimresb  15513  summo  15667  fsum2dlem  15720  prodmo  15884  fprod2dlem  15928  bezoutlem3  16487  bezoutlem4  16488  ncoprmgcdne1b  16591  qredeu  16599  coprmproddvdslem  16603  prmdvdsncoprmbd  16667  pcqmul  16790  pcadd  16826  pockthg  16843  prmreclem2  16854  vdwlem10  16927  ramub1lem2  16964  prmgaplem6  16993  prmgaplem7  16994  cshwsdisj  17036  mreexexlem4d  17595  mreexdomd  17597  issubc3  17803  cofucl  17842  setcmon  18041  setcepi  18042  drsdirfi  18262  poslubmo  18368  posglbmo  18369  grprida  18600  rabsubmgmd  18629  issubmd  18723  mndind  18745  ghmpreima  19152  gaorber  19213  psgnunilem4  19406  psgneu  19415  odcau  19513  pgpssslw  19523  fislw  19534  lsmsubm  19562  efgsfo  19648  gsum2d2  19883  pgpfac1lem5  19990  pgpfac1  19991  pgpfaclem2  19993  pgpfaclem3  19994  unitgrp  20274  lmodprop2d  20678  lsspropd  20772  lbsextlem4  20919  assapropd  21645  evlslem1  21864  mdetunilem8  22341  mdetuni0  22343  mdetmul  22345  neiint  22828  restbas  22882  iscnp4  22987  cnpco  22991  nrmsep  23081  regsep2  23100  ordthauslem  23107  1stcfb  23169  1stcrest  23177  2ndcctbss  23179  2ndcdisj  23180  2ndcomap  23182  dis2ndc  23184  nlly2i  23200  islly2  23208  hausllycmp  23218  lly1stc  23220  comppfsc  23256  ptbasin  23301  txcls  23328  ptcnp  23346  txlly  23360  txnlly  23361  txtube  23364  txcmplem1  23365  txcmplem2  23366  xkococnlem  23383  basqtop  23435  regr1lem  23463  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  reghmph  23517  nrmhmph  23518  opnfbas  23566  rnelfmlem  23676  fmufil  23683  fclscf  23749  fclsfnflim  23751  flimfnfcls  23752  uffclsflim  23755  cnpfcfi  23764  cnpfcf  23765  alexsubALTlem2  23772  alexsubALTlem4  23774  tgpconncompeqg  23836  ghmcnp  23839  qustgplem  23845  tsmsxp  23879  blssps  24150  blss  24151  blcld  24234  metequiv2  24239  met2ndci  24251  prdsxmslem2  24258  txmetcnp  24276  nlmvscnlem1  24423  xrge0tsms  24570  ipcnlem1  24986  iscmet3  25034  metsscmetcld  25056  minveclem3  25170  pmltpc  25191  ovolscalem2  25255  ovolicc2lem5  25262  ovolicc2  25263  nulmbl2  25277  ioombl1  25303  uniioombllem6  25329  uniioombl  25330  vitalilem3  25351  i1faddlem  25434  mbfmullem  25467  itg2split  25491  lhop2  25756  dvfsumrlim  25772  itgsubst  25790  plydivex  26034  plyexmo  26050  ulmbdd  26134  cxploglim  26706  dchrptlem2  26992  lgsquad2lem2  27112  2sqlem5  27149  dchrvmasumif  27230  rpvmasum2  27239  dchrisum0re  27240  dchrisum0lem3  27246  dchrisum0  27247  dchrmusum  27251  dchrvmasum  27252  pntibndlem3  27319  pntlemp  27337  ostth3  27365  nosupbday  27432  nosupbnd1lem1  27435  nosupbnd2  27443  noinfno  27445  noinfbday  27447  noinfbnd1lem1  27450  noinfbnd2  27458  conway  27525  madebdaylemlrcut  27618  mulsproplem9  27807  mulsproplem13  27811  mulsproplem14  27812  mulsuniflem  27831  legtrid  28097  hlcgreu  28124  mirreu3  28160  midexlem  28198  opphllem  28241  mideulem  28242  opphllem1  28253  oppperpex  28259  lnperpex  28309  trgcopy  28310  iscgra1  28316  cgraswap  28326  cgracom  28328  cgratr  28329  flatcgra  28330  acopyeu  28340  ax5seglem9  28450  ax5seg  28451  axcontlem8  28484  axcontlem12  28488  clwwlknonwwlknonb  29614  2pthfrgr  29792  frgrnbnb  29801  ablo4  30058  smcnlem  30205  pjhthmo  30810  mdslmd1lem1  31833  xrge0tsmsd  32467  locfinref  33107  xpinpreima2  33173  qqhval2  33248  dya2iocnrect  33566  orvcgteel  33752  orvclteel  33757  derangenlem  34448  cnpconn  34507  txpconn  34509  connpconn  34512  pconnpi1  34514  iccllysconn  34527  rellysconn  34528  cvmcov2  34552  cvmliftmolem2  34559  cvmliftmo  34561  cvmliftlem15  34575  cvmliftpht  34595  cvmlift3lem2  34597  cgrextend  35272  btwnouttr2  35286  cgrsub  35309  cgrxfr  35319  btwnxfr  35320  colineardim1  35325  btwnconn1lem6  35356  btwnconn1lem13  35363  btwnconn1lem14  35364  btwnconn3  35367  seglecgr12im  35374  segleantisym  35379  outsideofeq  35394  outsidele  35396  lineunray  35411  linethru  35417  fnessref  35545  neibastop2lem  35548  neibastop2  35549  unblimceq0lem  35685  knoppndvlem22  35712  bj-finsumval0  36469  isbasisrelowllem1  36539  isbasisrelowllem2  36540  mblfinlem3  36830  cnambfre  36839  areacirclem5  36883  istotbnd3  36942  sstotbnd  36946  crngm4  37174  cvlcvr1  38512  4atlem12  38786  paddasslem10  39003  paddasslem12  39005  paddasslem13  39006  lhpexle3lem  39185  cdlemd4  39375  cdleme0cq  39389  cdlemefs32sn1aw  39588  cdleme43fsv1snlem  39594  cdleme32d  39618  cdleme32f  39620  cdleme40m  39641  cdleme40n  39642  cdleme42keg  39660  cdleme42mgN  39662  cdleme50trn2  39725  cdleme50trn3  39727  cdlemm10N  40292  dihvalcqpre  40409  dihopelvalcpre  40422  dihmeetlem1N  40464  dihjat1lem  40602  mapd0  40839  mapdh9a  40963  fsuppssind  41467  nna4b4nsq  41704  diophin  41812  pellexlem3  41871  pellexlem5  41873  pellex  41875  pell14qrmulcl  41903  jm2.19lem3  42032  jm2.25  42040  jm2.27b  42047  lmhmfgsplit  42130  hbtlem2  42168  hbtlem5  42172  gsumws3  43250  gsumws4  43251  mnuprdlem4  43336  fnchoice  44015  stoweidlem17  45032  stoweidlem53  45068  stoweidlem61  45076  qndenserrnbllem  45309  bgoldbtbnd  46776  lindslinindsimp1  47226  prsthinc  47762