Theorem simprrl 781

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 730	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  4849  f1prex  7232  fpr3g  8228  fprresex  8253  nnaordex2  8568  naddssim  8614  eroveu  8752  mapdom2  9079  domunfican  9225  fofinf1o  9235  finsschain  9262  wemaplem3  9456  oemapvali  9596  iunfictbso  10027  enfin2i  10234  fin1a2s  10327  ttukeylem6  10427  distrlem4pr  10940  mulcmpblnr  10985  prsrlem1  10986  dedekind  11300  divdivdiv  11847  divmuleq  11851  divsubdiv  11862  lediv12a  12040  xralrple  13148  ssfzo12bi  13707  seqcaopr  13992  leexp2r  14127  hashbclem  14405  wrd2ind  14676  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  rtrclind  15018  rlimresb  15518  summo  15670  fsum2dlem  15723  prodmo  15892  fprod2dlem  15936  bezoutlem3  16501  bezoutlem4  16502  ncoprmgcdne1b  16610  qredeu  16618  coprmproddvdslem  16622  prmdvdsncoprmbd  16688  pcqmul  16815  pcadd  16851  pockthg  16868  prmreclem2  16879  vdwlem10  16952  ramub1lem2  16989  prmgaplem6  17018  prmgaplem7  17019  cshwsdisj  17060  mreexexlem4d  17604  mreexdomd  17606  issubc3  17807  cofucl  17846  setcmon  18045  setcepi  18046  drsdirfi  18262  poslubmo  18366  posglbmo  18367  grprida  18634  rabsubmgmd  18663  issubmd  18765  mndind  18787  ghmpreima  19204  gaorber  19274  psgnunilem4  19463  psgneu  19472  odcau  19570  pgpssslw  19580  fislw  19591  lsmsubm  19619  efgsfo  19705  gsum2d2  19940  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem2  20050  pgpfaclem3  20051  unitgrp  20354  lmodprop2d  20910  lsspropd  21004  lbsextlem4  21151  assapropd  21861  evlslem1  22070  mdetunilem8  22594  mdetuni0  22596  mdetmul  22598  neiint  23079  restbas  23133  iscnp4  23238  cnpco  23242  nrmsep  23332  regsep2  23351  ordthauslem  23358  1stcfb  23420  1stcrest  23428  2ndcctbss  23430  2ndcdisj  23431  2ndcomap  23433  dis2ndc  23435  nlly2i  23451  islly2  23459  hausllycmp  23469  lly1stc  23471  comppfsc  23507  ptbasin  23552  txcls  23579  ptcnp  23597  txlly  23611  txnlly  23612  txtube  23615  txcmplem1  23616  txcmplem2  23617  xkococnlem  23634  basqtop  23686  regr1lem  23714  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  reghmph  23768  nrmhmph  23769  opnfbas  23817  rnelfmlem  23927  fmufil  23934  fclscf  24000  fclsfnflim  24002  flimfnfcls  24003  uffclsflim  24006  cnpfcfi  24015  cnpfcf  24016  alexsubALTlem2  24023  alexsubALTlem4  24025  tgpconncompeqg  24087  ghmcnp  24090  qustgplem  24096  tsmsxp  24130  blssps  24399  blss  24400  blcld  24480  metequiv2  24485  met2ndci  24497  prdsxmslem2  24504  txmetcnp  24522  nlmvscnlem1  24661  xrge0tsms  24810  ipcnlem1  25222  iscmet3  25270  metsscmetcld  25292  minveclem3  25406  pmltpc  25427  ovolscalem2  25491  ovolicc2lem5  25498  ovolicc2  25499  nulmbl2  25513  ioombl1  25539  uniioombllem6  25565  uniioombl  25566  vitalilem3  25587  i1faddlem  25670  mbfmullem  25702  itg2split  25726  lhop2  25992  dvfsumrlim  26008  itgsubst  26026  plydivex  26274  plyexmo  26290  ulmbdd  26376  cxploglim  26955  dchrptlem2  27242  lgsquad2lem2  27362  2sqlem5  27399  dchrvmasumif  27480  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem3  27496  dchrisum0  27497  dchrmusum  27501  dchrvmasum  27502  pntibndlem3  27569  pntlemp  27587  ostth3  27615  nosupbday  27683  nosupbnd1lem1  27686  nosupbnd2  27694  noinfno  27696  noinfbday  27698  noinfbnd1lem1  27701  noinfbnd2  27709  conway  27785  madebdaylemlrcut  27905  mulsproplem9  28130  mulsproplem13  28134  mulsproplem14  28135  mulsuniflem  28155  uzsind  28411  bdayfinbndlem1  28473  readdscl  28505  legtrid  28673  hlcgreu  28700  mirreu3  28736  midexlem  28774  opphllem  28817  mideulem  28818  opphllem1  28829  oppperpex  28835  lnperpex  28885  trgcopy  28886  iscgra1  28892  cgraswap  28902  cgracom  28904  cgratr  28905  flatcgra  28906  acopyeu  28916  ax5seglem9  29020  ax5seg  29021  axcontlem8  29054  axcontlem12  29058  clwwlknonwwlknonb  30191  2pthfrgr  30369  frgrnbnb  30378  ablo4  30636  smcnlem  30783  pjhthmo  31388  mdslmd1lem1  32411  xrge0tsmsd  33149  locfinref  34001  xpinpreima2  34067  qqhval2  34142  dya2iocnrect  34441  orvcgteel  34628  orvclteel  34633  derangenlem  35369  cnpconn  35428  txpconn  35430  connpconn  35433  pconnpi1  35435  iccllysconn  35448  rellysconn  35449  cvmcov2  35473  cvmliftmolem2  35480  cvmliftmo  35482  cvmliftlem15  35496  cvmliftpht  35516  cvmlift3lem2  35518  cgrextend  36206  btwnouttr2  36220  cgrsub  36243  cgrxfr  36253  btwnxfr  36254  colineardim1  36259  btwnconn1lem6  36290  btwnconn1lem13  36297  btwnconn1lem14  36298  btwnconn3  36301  seglecgr12im  36308  segleantisym  36313  outsideofeq  36328  outsidele  36330  lineunray  36345  linethru  36351  fnessref  36555  neibastop2lem  36558  neibastop2  36559  weiunpo  36663  unblimceq0lem  36782  knoppndvlem22  36809  bj-finsumval0  37615  isbasisrelowllem1  37685  isbasisrelowllem2  37686  mblfinlem3  37994  cnambfre  38003  areacirclem5  38047  istotbnd3  38106  sstotbnd  38110  crngm4  38338  cvlcvr1  39799  4atlem12  40072  paddasslem10  40289  paddasslem12  40291  paddasslem13  40292  lhpexle3lem  40471  cdlemd4  40661  cdleme0cq  40675  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdleme32d  40904  cdleme32f  40906  cdleme40m  40927  cdleme40n  40928  cdleme42keg  40946  cdleme42mgN  40948  cdleme50trn2  41011  cdleme50trn3  41013  cdlemm10N  41578  dihvalcqpre  41695  dihopelvalcpre  41708  dihmeetlem1N  41750  dihjat1lem  41888  mapd0  42125  mapdh9a  42249  fsuppssind  43040  nna4b4nsq  43107  diophin  43218  pellexlem3  43277  pellexlem5  43279  pellex  43281  pell14qrmulcl  43309  jm2.19lem3  43437  jm2.25  43445  jm2.27b  43452  lmhmfgsplit  43532  hbtlem2  43570  hbtlem5  43574  gsumws3  44641  gsumws4  44642  mnuprdlem4  44720  fnchoice  45478  stoweidlem17  46463  stoweidlem53  46499  stoweidlem61  46507  qndenserrnbllem  46740  bgoldbtbnd  48297  cycldlenngric  48416  isubgr3stgrlem6  48459  lindslinindsimp1  48945  brab2dd  49315  prsthinc  49951