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  4856  f1prex  7224  fpr3g  8221  fprresex  8246  nnaordex2  8560  naddssim  8606  eroveu  8742  mapdom2  9068  domunfican  9213  fofinf1o  9223  finsschain  9250  wemaplem3  9441  oemapvali  9581  iunfictbso  10012  enfin2i  10219  fin1a2s  10312  ttukeylem6  10412  distrlem4pr  10924  mulcmpblnr  10969  prsrlem1  10970  dedekind  11283  divdivdiv  11829  divmuleq  11833  divsubdiv  11844  lediv12a  12022  xralrple  13106  ssfzo12bi  13663  seqcaopr  13948  leexp2r  14083  hashbclem  14361  wrd2ind  14632  rtrclreclem3  14969  rtrclreclem4  14970  relexpindlem  14972  rtrclind  14974  rlimresb  15474  summo  15626  fsum2dlem  15679  prodmo  15845  fprod2dlem  15889  bezoutlem3  16454  bezoutlem4  16455  ncoprmgcdne1b  16563  qredeu  16571  coprmproddvdslem  16575  prmdvdsncoprmbd  16640  pcqmul  16767  pcadd  16803  pockthg  16820  prmreclem2  16831  vdwlem10  16904  ramub1lem2  16941  prmgaplem6  16970  prmgaplem7  16971  cshwsdisj  17012  mreexexlem4d  17555  mreexdomd  17557  issubc3  17758  cofucl  17797  setcmon  17996  setcepi  17997  drsdirfi  18213  poslubmo  18317  posglbmo  18318  grprida  18585  rabsubmgmd  18614  issubmd  18716  mndind  18738  ghmpreima  19152  gaorber  19222  psgnunilem4  19411  psgneu  19420  odcau  19518  pgpssslw  19528  fislw  19539  lsmsubm  19567  efgsfo  19653  gsum2d2  19888  pgpfac1lem5  19995  pgpfac1  19996  pgpfaclem2  19998  pgpfaclem3  19999  unitgrp  20303  lmodprop2d  20859  lsspropd  20953  lbsextlem4  21100  assapropd  21811  evlslem1  22018  mdetunilem8  22535  mdetuni0  22537  mdetmul  22539  neiint  23020  restbas  23074  iscnp4  23179  cnpco  23183  nrmsep  23273  regsep2  23292  ordthauslem  23299  1stcfb  23361  1stcrest  23369  2ndcctbss  23371  2ndcdisj  23372  2ndcomap  23374  dis2ndc  23376  nlly2i  23392  islly2  23400  hausllycmp  23410  lly1stc  23412  comppfsc  23448  ptbasin  23493  txcls  23520  ptcnp  23538  txlly  23552  txnlly  23553  txtube  23556  txcmplem1  23557  txcmplem2  23558  xkococnlem  23575  basqtop  23627  regr1lem  23655  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  reghmph  23709  nrmhmph  23710  opnfbas  23758  rnelfmlem  23868  fmufil  23875  fclscf  23941  fclsfnflim  23943  flimfnfcls  23944  uffclsflim  23947  cnpfcfi  23956  cnpfcf  23957  alexsubALTlem2  23964  alexsubALTlem4  23966  tgpconncompeqg  24028  ghmcnp  24031  qustgplem  24037  tsmsxp  24071  blssps  24340  blss  24341  blcld  24421  metequiv2  24426  met2ndci  24438  prdsxmslem2  24445  txmetcnp  24463  nlmvscnlem1  24602  xrge0tsms  24751  ipcnlem1  25173  iscmet3  25221  metsscmetcld  25243  minveclem3  25357  pmltpc  25379  ovolscalem2  25443  ovolicc2lem5  25450  ovolicc2  25451  nulmbl2  25465  ioombl1  25491  uniioombllem6  25517  uniioombl  25518  vitalilem3  25539  i1faddlem  25622  mbfmullem  25654  itg2split  25678  lhop2  25948  dvfsumrlim  25966  itgsubst  25984  plydivex  26233  plyexmo  26249  ulmbdd  26335  cxploglim  26916  dchrptlem2  27204  lgsquad2lem2  27324  2sqlem5  27361  dchrvmasumif  27442  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem3  27458  dchrisum0  27459  dchrmusum  27463  dchrvmasum  27464  pntibndlem3  27531  pntlemp  27549  ostth3  27577  nosupbday  27645  nosupbnd1lem1  27648  nosupbnd2  27656  noinfno  27658  noinfbday  27660  noinfbnd1lem1  27663  noinfbnd2  27671  conway  27741  madebdaylemlrcut  27845  mulsproplem9  28064  mulsproplem13  28068  mulsproplem14  28069  mulsuniflem  28089  uzsind  28330  readdscl  28402  legtrid  28570  hlcgreu  28597  mirreu3  28633  midexlem  28671  opphllem  28714  mideulem  28715  opphllem1  28726  oppperpex  28732  lnperpex  28782  trgcopy  28783  iscgra1  28789  cgraswap  28799  cgracom  28801  cgratr  28802  flatcgra  28803  acopyeu  28813  ax5seglem9  28917  ax5seg  28918  axcontlem8  28951  axcontlem12  28955  clwwlknonwwlknonb  30088  2pthfrgr  30266  frgrnbnb  30275  ablo4  30532  smcnlem  30679  pjhthmo  31284  mdslmd1lem1  32307  xrge0tsmsd  33049  locfinref  33875  xpinpreima2  33941  qqhval2  34016  dya2iocnrect  34315  orvcgteel  34502  orvclteel  34507  derangenlem  35236  cnpconn  35295  txpconn  35297  connpconn  35300  pconnpi1  35302  iccllysconn  35315  rellysconn  35316  cvmcov2  35340  cvmliftmolem2  35347  cvmliftmo  35349  cvmliftlem15  35363  cvmliftpht  35383  cvmlift3lem2  35385  cgrextend  36073  btwnouttr2  36087  cgrsub  36110  cgrxfr  36120  btwnxfr  36121  colineardim1  36126  btwnconn1lem6  36157  btwnconn1lem13  36164  btwnconn1lem14  36165  btwnconn3  36168  seglecgr12im  36175  segleantisym  36180  outsideofeq  36195  outsidele  36197  lineunray  36212  linethru  36218  fnessref  36422  neibastop2lem  36425  neibastop2  36426  weiunpo  36530  unblimceq0lem  36571  knoppndvlem22  36598  bj-finsumval0  37350  isbasisrelowllem1  37420  isbasisrelowllem2  37421  mblfinlem3  37719  cnambfre  37728  areacirclem5  37772  istotbnd3  37831  sstotbnd  37835  crngm4  38063  cvlcvr1  39458  4atlem12  39731  paddasslem10  39948  paddasslem12  39950  paddasslem13  39951  lhpexle3lem  40130  cdlemd4  40320  cdleme0cq  40334  cdlemefs32sn1aw  40533  cdleme43fsv1snlem  40539  cdleme32d  40563  cdleme32f  40565  cdleme40m  40586  cdleme40n  40587  cdleme42keg  40605  cdleme42mgN  40607  cdleme50trn2  40670  cdleme50trn3  40672  cdlemm10N  41237  dihvalcqpre  41354  dihopelvalcpre  41367  dihmeetlem1N  41409  dihjat1lem  41547  mapd0  41784  mapdh9a  41908  fsuppssind  42711  nna4b4nsq  42778  diophin  42889  pellexlem3  42948  pellexlem5  42950  pellex  42952  pell14qrmulcl  42980  jm2.19lem3  43108  jm2.25  43116  jm2.27b  43123  lmhmfgsplit  43203  hbtlem2  43241  hbtlem5  43245  gsumws3  44313  gsumws4  44314  mnuprdlem4  44392  fnchoice  45150  stoweidlem17  46139  stoweidlem53  46175  stoweidlem61  46183  qndenserrnbllem  46416  bgoldbtbnd  47933  cycldlenngric  48052  isubgr3stgrlem6  48095  lindslinindsimp1  48582  brab2dd  48952  prsthinc  49589