Theorem simprrl 786

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 735	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 208  df-an 397

This theorem is referenced by:  prproe  4843  f1prex  7235  fpr3g  8232  fprresex  8257  nnaordex2  8572  naddssim  8618  eroveu  8756  mapdom2  9083  domunfican  9229  fofinf1o  9239  finsschain  9266  wemaplem3  9460  oemapvali  9603  iunfictbso  10034  enfin2i  10241  fin1a2s  10334  ttukeylem6  10434  distrlem4pr  10947  mulcmpblnr  10992  prsrlem1  10993  dedekind  11307  divdivdiv  11854  divmuleq  11858  divsubdiv  11869  lediv12a  12047  xralrple  13155  ssfzo12bi  13714  seqcaopr  13999  leexp2r  14134  hashbclem  14412  wrd2ind  14683  rtrclreclem3  15020  rtrclreclem4  15021  relexpindlem  15023  rtrclind  15025  rlimresb  15525  summo  15677  fsum2dlem  15730  prodmo  15899  fprod2dlem  15943  bezoutlem3  16508  bezoutlem4  16509  ncoprmgcdne1b  16617  qredeu  16625  coprmproddvdslem  16629  prmdvdsncoprmbd  16695  pcqmul  16822  pcadd  16858  pockthg  16875  prmreclem2  16886  vdwlem10  16959  ramub1lem2  16996  prmgaplem6  17025  prmgaplem7  17026  cshwsdisj  17067  mreexexlem4d  17611  mreexdomd  17613  issubc3  17814  cofucl  17853  setcmon  18052  setcepi  18053  drsdirfi  18269  poslubmo  18373  posglbmo  18374  grprida  18641  rabsubmgmd  18670  issubmd  18772  mndind  18794  ghmpreima  19211  gaorber  19281  psgnunilem4  19470  psgneu  19479  odcau  19577  pgpssslw  19587  fislw  19598  lsmsubm  19626  efgsfo  19712  gsum2d2  19947  pgpfac1lem5  20054  pgpfac1  20055  pgpfaclem2  20057  pgpfaclem3  20058  unitgrp  20361  lmodprop2d  20921  lsspropd  21014  lbsextlem4  21161  assapropd  21853  evlslem1  22065  mdetunilem8  22609  mdetuni0  22611  mdetmul  22613  neiint  23094  restbas  23148  iscnp4  23253  cnpco  23257  nrmsep  23347  regsep2  23366  ordthauslem  23373  1stcfb  23435  1stcrest  23443  2ndcctbss  23445  2ndcdisj  23446  2ndcomap  23448  dis2ndc  23450  nlly2i  23466  islly2  23474  hausllycmp  23484  lly1stc  23486  comppfsc  23522  ptbasin  23567  txcls  23594  ptcnp  23612  txlly  23626  txnlly  23627  txtube  23630  txcmplem1  23631  txcmplem2  23632  xkococnlem  23649  basqtop  23701  regr1lem  23729  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  reghmph  23783  nrmhmph  23784  opnfbas  23832  rnelfmlem  23942  fmufil  23949  fclscf  24015  fclsfnflim  24017  flimfnfcls  24018  uffclsflim  24021  cnpfcfi  24030  cnpfcf  24031  alexsubALTlem2  24038  alexsubALTlem4  24040  tgpconncompeqg  24102  ghmcnp  24105  qustgplem  24111  tsmsxp  24145  blssps  24414  blss  24415  blcld  24495  metequiv2  24500  met2ndci  24512  prdsxmslem2  24519  txmetcnp  24537  nlmvscnlem1  24676  xrge0tsms  24825  ipcnlem1  25237  iscmet3  25285  metsscmetcld  25307  minveclem3  25421  pmltpc  25442  ovolscalem2  25506  ovolicc2lem5  25513  ovolicc2  25514  nulmbl2  25528  ioombl1  25554  uniioombllem6  25580  uniioombl  25581  vitalilem3  25602  i1faddlem  25685  mbfmullem  25717  itg2split  25741  lhop2  26007  dvfsumrlim  26023  itgsubst  26041  plydivex  26288  plyexmo  26304  ulmbdd  26388  cxploglim  26966  dchrptlem2  27253  lgsquad2lem2  27373  2sqlem5  27410  dchrvmasumif  27491  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem3  27507  dchrisum0  27508  dchrmusum  27512  dchrvmasum  27513  pntibndlem3  27580  pntlemp  27598  ostth3  27626  nosupbday  27694  nosupbnd1lem1  27697  nosupbnd2  27705  noinfno  27707  noinfbday  27709  noinfbnd1lem1  27712  noinfbnd2  27720  conway  27796  madebdaylemlrcut  27916  mulsproplem9  28141  mulsproplem13  28145  mulsproplem14  28146  mulsuniflem  28166  uzsind  28422  bdayfinbndlem1  28484  readdscl  28516  legtrid  28684  hlcgreu  28711  mirreu3  28747  midexlem  28785  opphllem  28828  mideulem  28829  opphllem1  28840  oppperpex  28846  lnperpex  28896  trgcopy  28897  iscgra1  28903  cgraswap  28913  cgracom  28915  cgratr  28916  flatcgra  28917  acopyeu  28927  ax5seglem9  29031  ax5seg  29032  axcontlem8  29065  axcontlem12  29069  clwwlknonwwlknonb  30201  2pthfrgr  30379  frgrnbnb  30388  ablo4  30646  smcnlem  30793  pjhthmo  31398  mdslmd1lem1  32421  xrge0tsmsd  33161  locfinref  34032  xpinpreima2  34098  qqhval2  34173  dya2iocnrect  34472  orvcgteel  34659  orvclteel  34664  derangenlem  35406  cnpconn  35465  txpconn  35467  connpconn  35470  pconnpi1  35472  iccllysconn  35485  rellysconn  35486  cvmcov2  35510  cvmliftmolem2  35517  cvmliftmo  35519  cvmliftlem15  35533  cvmliftpht  35553  cvmlift3lem2  35555  cgrextend  36243  btwnouttr2  36257  cgrsub  36280  cgrxfr  36290  btwnxfr  36291  colineardim1  36296  btwnconn1lem6  36327  btwnconn1lem13  36334  btwnconn1lem14  36335  btwnconn3  36338  seglecgr12im  36345  segleantisym  36350  outsideofeq  36365  outsidele  36367  lineunray  36382  linethru  36388  fnessref  36592  neibastop2lem  36595  neibastop2  36596  weiunpo  36700  unblimceq0lem  36819  knoppndvlem22  36846  bj-finsumval0  37652  isbasisrelowllem1  37724  isbasisrelowllem2  37725  mblfinlem3  38033  cnambfre  38042  areacirclem5  38086  istotbnd3  38145  sstotbnd  38149  crngm4  38377  cvlcvr1  39838  4atlem12  40111  paddasslem10  40328  paddasslem12  40330  paddasslem13  40331  lhpexle3lem  40510  cdlemd4  40700  cdleme0cq  40714  cdlemefs32sn1aw  40913  cdleme43fsv1snlem  40919  cdleme32d  40943  cdleme32f  40945  cdleme40m  40966  cdleme40n  40967  cdleme42keg  40985  cdleme42mgN  40987  cdleme50trn2  41050  cdleme50trn3  41052  cdlemm10N  41617  dihvalcqpre  41734  dihopelvalcpre  41747  dihmeetlem1N  41789  dihjat1lem  41927  mapd0  42164  mapdh9a  42288  fsuppssind  43050  nna4b4nsq  43117  diophin  43228  pellexlem3  43283  pellexlem5  43285  pellex  43287  pell14qrmulcl  43315  jm2.19lem3  43443  jm2.25  43451  jm2.27b  43458  lmhmfgsplit  43538  hbtlem2  43576  hbtlem5  43580  gsumws3  44647  gsumws4  44648  mnuprdlem4  44726  fnchoice  45484  stoweidlem17  46467  stoweidlem53  46503  stoweidlem61  46511  qndenserrnbllem  46744  bgoldbtbnd  48307  cycldlenngric  48426  isubgr3stgrlem6  48469  lindslinindsimp1  48955  brab2dd  49325  prsthinc  49961