Theorem simprrl 777

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 725	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 206  df-an 396

This theorem is referenced by:  prproe  4842  f1prex  7149  fpr3g  8085  fprresex  8110  wfrlem17OLD  8140  eroveu  8575  undom  8816  mapdom2  8900  domunfican  9048  fofinf1o  9055  finsschain  9087  wemaplem3  9268  oemapvali  9403  iunfictbso  9854  enfin2i  10061  fin1a2s  10154  ttukeylem6  10254  distrlem4pr  10766  mulcmpblnr  10811  prsrlem1  10812  dedekind  11121  divdivdiv  11659  divmuleq  11663  divsubdiv  11674  lediv12a  11851  xralrple  12921  ssfzo12bi  13463  seqcaopr  13741  leexp2r  13873  hashbclem  14145  wrd2ind  14417  rtrclreclem3  14752  rtrclreclem4  14753  relexpindlem  14755  rtrclind  14757  rlimresb  15255  summo  15410  fsum2dlem  15463  prodmo  15627  fprod2dlem  15671  bezoutlem3  16230  bezoutlem4  16231  ncoprmgcdne1b  16336  qredeu  16344  coprmproddvdslem  16348  prmdvdsncoprmbd  16412  pcqmul  16535  pcadd  16571  pockthg  16588  prmreclem2  16599  vdwlem10  16672  ramub1lem2  16709  prmgaplem6  16738  prmgaplem7  16739  cshwsdisj  16781  mreexexlem4d  17337  mreexdomd  17339  issubc3  17545  cofucl  17584  setcmon  17783  setcepi  17784  drsdirfi  18004  poslubmo  18110  posglbmo  18111  grpridd  18340  issubmd  18426  mndind  18447  ghmpreima  18837  gaorber  18895  psgnunilem4  19086  psgneu  19095  odcau  19190  pgpssslw  19200  fislw  19211  lsmsubm  19239  efgsfo  19326  gsum2d2  19556  pgpfac1lem5  19663  pgpfac1  19664  pgpfaclem2  19666  pgpfaclem3  19667  unitgrp  19890  lmodprop2d  20166  lsspropd  20260  lbsextlem4  20404  assapropd  21057  evlslem1  21273  mdetunilem8  21749  mdetuni0  21751  mdetmul  21753  neiint  22236  restbas  22290  iscnp4  22395  cnpco  22399  nrmsep  22489  regsep2  22508  ordthauslem  22515  1stcfb  22577  1stcrest  22585  2ndcctbss  22587  2ndcdisj  22588  2ndcomap  22590  dis2ndc  22592  nlly2i  22608  islly2  22616  hausllycmp  22626  lly1stc  22628  comppfsc  22664  ptbasin  22709  txcls  22736  ptcnp  22754  txlly  22768  txnlly  22769  txtube  22772  txcmplem1  22773  txcmplem2  22774  xkococnlem  22791  basqtop  22843  regr1lem  22871  kqreglem1  22873  kqreglem2  22874  kqnrmlem1  22875  kqnrmlem2  22876  reghmph  22925  nrmhmph  22926  opnfbas  22974  rnelfmlem  23084  fmufil  23091  fclscf  23157  fclsfnflim  23159  flimfnfcls  23160  uffclsflim  23163  cnpfcfi  23172  cnpfcf  23173  alexsubALTlem2  23180  alexsubALTlem4  23182  tgpconncompeqg  23244  ghmcnp  23247  qustgplem  23253  tsmsxp  23287  blssps  23558  blss  23559  blcld  23642  metequiv2  23647  met2ndci  23659  prdsxmslem2  23666  txmetcnp  23684  nlmvscnlem1  23831  xrge0tsms  23978  ipcnlem1  24390  iscmet3  24438  metsscmetcld  24460  minveclem3  24574  pmltpc  24595  ovolscalem2  24659  ovolicc2lem5  24666  ovolicc2  24667  nulmbl2  24681  ioombl1  24707  uniioombllem6  24733  uniioombl  24734  vitalilem3  24755  i1faddlem  24838  mbfmullem  24871  itg2split  24895  lhop2  25160  dvfsumrlim  25176  itgsubst  25194  plydivex  25438  plyexmo  25454  ulmbdd  25538  cxploglim  26108  dchrptlem2  26394  lgsquad2lem2  26514  2sqlem5  26551  dchrvmasumif  26632  rpvmasum2  26641  dchrisum0re  26642  dchrisum0lem3  26648  dchrisum0  26649  dchrmusum  26653  dchrvmasum  26654  pntibndlem3  26721  pntlemp  26739  ostth3  26767  legtrid  26933  hlcgreu  26960  mirreu3  26996  midexlem  27034  opphllem  27077  mideulem  27078  opphllem1  27089  oppperpex  27095  lnperpex  27145  trgcopy  27146  iscgra1  27152  cgraswap  27162  cgracom  27164  cgratr  27165  flatcgra  27166  acopyeu  27176  ax5seglem9  27286  ax5seg  27287  axcontlem8  27320  axcontlem12  27324  clwwlknonwwlknonb  28449  2pthfrgr  28627  frgrnbnb  28636  ablo4  28891  smcnlem  29038  pjhthmo  29643  mdslmd1lem1  30666  xrge0tsmsd  31296  locfinref  31770  xpinpreima2  31836  qqhval2  31911  dya2iocnrect  32227  orvcgteel  32413  orvclteel  32418  derangenlem  33112  cnpconn  33171  txpconn  33173  connpconn  33176  pconnpi1  33178  iccllysconn  33191  rellysconn  33192  cvmcov2  33216  cvmliftmolem2  33223  cvmliftmo  33225  cvmliftlem15  33239  cvmliftpht  33259  cvmlift3lem2  33261  naddssim  33816  nosupbday  33887  nosupbnd1lem1  33890  nosupbnd2  33898  noinfno  33900  noinfbday  33902  noinfbnd1lem1  33905  noinfbnd2  33913  conway  33972  madebdaylemlrcut  34058  cgrextend  34289  btwnouttr2  34303  cgrsub  34326  cgrxfr  34336  btwnxfr  34337  colineardim1  34342  btwnconn1lem6  34373  btwnconn1lem13  34380  btwnconn1lem14  34381  btwnconn3  34384  seglecgr12im  34391  segleantisym  34396  outsideofeq  34411  outsidele  34413  lineunray  34428  linethru  34434  fnessref  34525  neibastop2lem  34528  neibastop2  34529  unblimceq0lem  34665  knoppndvlem22  34692  bj-finsumval0  35435  isbasisrelowllem1  35505  isbasisrelowllem2  35506  mblfinlem3  35795  cnambfre  35804  areacirclem5  35848  istotbnd3  35908  sstotbnd  35912  crngm4  36140  cvlcvr1  37332  4atlem12  37605  paddasslem10  37822  paddasslem12  37824  paddasslem13  37825  lhpexle3lem  38004  cdlemd4  38194  cdleme0cq  38208  cdlemefs32sn1aw  38407  cdleme43fsv1snlem  38413  cdleme32d  38437  cdleme32f  38439  cdleme40m  38460  cdleme40n  38461  cdleme42keg  38479  cdleme42mgN  38481  cdleme50trn2  38544  cdleme50trn3  38546  cdlemm10N  39111  dihvalcqpre  39228  dihopelvalcpre  39241  dihmeetlem1N  39283  dihjat1lem  39421  mapd0  39658  mapdh9a  39782  fsuppssind  40262  nna4b4nsq  40477  diophin  40574  pellexlem3  40633  pellexlem5  40635  pellex  40637  pell14qrmulcl  40665  jm2.19lem3  40793  jm2.25  40801  jm2.27b  40808  lmhmfgsplit  40891  hbtlem2  40929  hbtlem5  40933  gsumws3  41760  gsumws4  41761  mnuprdlem4  41846  fnchoice  42525  stoweidlem17  43512  stoweidlem53  43548  stoweidlem61  43556  qndenserrnbllem  43789  bgoldbtbnd  45213  rabsubmgmd  45297  lindslinindsimp1  45750  prsthinc  46287