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  4861  f1prex  7230  fpr3g  8227  fprresex  8252  nnaordex2  8567  naddssim  8613  eroveu  8749  mapdom2  9076  domunfican  9222  fofinf1o  9232  finsschain  9259  wemaplem3  9453  oemapvali  9593  iunfictbso  10024  enfin2i  10231  fin1a2s  10324  ttukeylem6  10424  distrlem4pr  10937  mulcmpblnr  10982  prsrlem1  10983  dedekind  11296  divdivdiv  11842  divmuleq  11846  divsubdiv  11857  lediv12a  12035  xralrple  13120  ssfzo12bi  13677  seqcaopr  13962  leexp2r  14097  hashbclem  14375  wrd2ind  14646  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  rtrclind  14988  rlimresb  15488  summo  15640  fsum2dlem  15693  prodmo  15859  fprod2dlem  15903  bezoutlem3  16468  bezoutlem4  16469  ncoprmgcdne1b  16577  qredeu  16585  coprmproddvdslem  16589  prmdvdsncoprmbd  16654  pcqmul  16781  pcadd  16817  pockthg  16834  prmreclem2  16845  vdwlem10  16918  ramub1lem2  16955  prmgaplem6  16984  prmgaplem7  16985  cshwsdisj  17026  mreexexlem4d  17570  mreexdomd  17572  issubc3  17773  cofucl  17812  setcmon  18011  setcepi  18012  drsdirfi  18228  poslubmo  18332  posglbmo  18333  grprida  18600  rabsubmgmd  18629  issubmd  18731  mndind  18753  ghmpreima  19167  gaorber  19237  psgnunilem4  19426  psgneu  19435  odcau  19533  pgpssslw  19543  fislw  19554  lsmsubm  19582  efgsfo  19668  gsum2d2  19903  pgpfac1lem5  20010  pgpfac1  20011  pgpfaclem2  20013  pgpfaclem3  20014  unitgrp  20319  lmodprop2d  20875  lsspropd  20969  lbsextlem4  21116  assapropd  21827  evlslem1  22037  mdetunilem8  22563  mdetuni0  22565  mdetmul  22567  neiint  23048  restbas  23102  iscnp4  23207  cnpco  23211  nrmsep  23301  regsep2  23320  ordthauslem  23327  1stcfb  23389  1stcrest  23397  2ndcctbss  23399  2ndcdisj  23400  2ndcomap  23402  dis2ndc  23404  nlly2i  23420  islly2  23428  hausllycmp  23438  lly1stc  23440  comppfsc  23476  ptbasin  23521  txcls  23548  ptcnp  23566  txlly  23580  txnlly  23581  txtube  23584  txcmplem1  23585  txcmplem2  23586  xkococnlem  23603  basqtop  23655  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  reghmph  23737  nrmhmph  23738  opnfbas  23786  rnelfmlem  23896  fmufil  23903  fclscf  23969  fclsfnflim  23971  flimfnfcls  23972  uffclsflim  23975  cnpfcfi  23984  cnpfcf  23985  alexsubALTlem2  23992  alexsubALTlem4  23994  tgpconncompeqg  24056  ghmcnp  24059  qustgplem  24065  tsmsxp  24099  blssps  24368  blss  24369  blcld  24449  metequiv2  24454  met2ndci  24466  prdsxmslem2  24473  txmetcnp  24491  nlmvscnlem1  24630  xrge0tsms  24779  ipcnlem1  25201  iscmet3  25249  metsscmetcld  25271  minveclem3  25385  pmltpc  25407  ovolscalem2  25471  ovolicc2lem5  25478  ovolicc2  25479  nulmbl2  25493  ioombl1  25519  uniioombllem6  25545  uniioombl  25546  vitalilem3  25567  i1faddlem  25650  mbfmullem  25682  itg2split  25706  lhop2  25976  dvfsumrlim  25994  itgsubst  26012  plydivex  26261  plyexmo  26277  ulmbdd  26363  cxploglim  26944  dchrptlem2  27232  lgsquad2lem2  27352  2sqlem5  27389  dchrvmasumif  27470  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem3  27486  dchrisum0  27487  dchrmusum  27491  dchrvmasum  27492  pntibndlem3  27559  pntlemp  27577  ostth3  27605  nosupbday  27673  nosupbnd1lem1  27676  nosupbnd2  27684  noinfno  27686  noinfbday  27688  noinfbnd1lem1  27691  noinfbnd2  27699  conway  27775  madebdaylemlrcut  27895  mulsproplem9  28120  mulsproplem13  28124  mulsproplem14  28125  mulsuniflem  28145  uzsind  28401  bdayfinbndlem1  28463  readdscl  28495  legtrid  28663  hlcgreu  28690  mirreu3  28726  midexlem  28764  opphllem  28807  mideulem  28808  opphllem1  28819  oppperpex  28825  lnperpex  28875  trgcopy  28876  iscgra1  28882  cgraswap  28892  cgracom  28894  cgratr  28895  flatcgra  28896  acopyeu  28906  ax5seglem9  29010  ax5seg  29011  axcontlem8  29044  axcontlem12  29048  clwwlknonwwlknonb  30181  2pthfrgr  30359  frgrnbnb  30368  ablo4  30625  smcnlem  30772  pjhthmo  31377  mdslmd1lem1  32400  xrge0tsmsd  33155  locfinref  33998  xpinpreima2  34064  qqhval2  34139  dya2iocnrect  34438  orvcgteel  34625  orvclteel  34630  derangenlem  35365  cnpconn  35424  txpconn  35426  connpconn  35429  pconnpi1  35431  iccllysconn  35444  rellysconn  35445  cvmcov2  35469  cvmliftmolem2  35476  cvmliftmo  35478  cvmliftlem15  35492  cvmliftpht  35512  cvmlift3lem2  35514  cgrextend  36202  btwnouttr2  36216  cgrsub  36239  cgrxfr  36249  btwnxfr  36250  colineardim1  36255  btwnconn1lem6  36286  btwnconn1lem13  36293  btwnconn1lem14  36294  btwnconn3  36297  seglecgr12im  36304  segleantisym  36309  outsideofeq  36324  outsidele  36326  lineunray  36341  linethru  36347  fnessref  36551  neibastop2lem  36554  neibastop2  36555  weiunpo  36659  unblimceq0lem  36706  knoppndvlem22  36733  bj-finsumval0  37486  isbasisrelowllem1  37556  isbasisrelowllem2  37557  mblfinlem3  37856  cnambfre  37865  areacirclem5  37909  istotbnd3  37968  sstotbnd  37972  crngm4  38200  cvlcvr1  39595  4atlem12  39868  paddasslem10  40085  paddasslem12  40087  paddasslem13  40088  lhpexle3lem  40267  cdlemd4  40457  cdleme0cq  40471  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdleme32d  40700  cdleme32f  40702  cdleme40m  40723  cdleme40n  40724  cdleme42keg  40742  cdleme42mgN  40744  cdleme50trn2  40807  cdleme50trn3  40809  cdlemm10N  41374  dihvalcqpre  41491  dihopelvalcpre  41504  dihmeetlem1N  41546  dihjat1lem  41684  mapd0  41921  mapdh9a  42045  fsuppssind  42832  nna4b4nsq  42899  diophin  43010  pellexlem3  43069  pellexlem5  43071  pellex  43073  pell14qrmulcl  43101  jm2.19lem3  43229  jm2.25  43237  jm2.27b  43244  lmhmfgsplit  43324  hbtlem2  43362  hbtlem5  43366  gsumws3  44433  gsumws4  44434  mnuprdlem4  44512  fnchoice  45270  stoweidlem17  46257  stoweidlem53  46293  stoweidlem61  46301  qndenserrnbllem  46534  bgoldbtbnd  48051  cycldlenngric  48170  isubgr3stgrlem6  48213  lindslinindsimp1  48699  brab2dd  49069  prsthinc  49705