Theorem simprrl 768

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 475	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 716	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  prproe  4704  f1prex  6859  grpridd  7198  wfrlem17  7769  eroveu  8186  undom  8395  mapdom2  8478  domunfican  8580  fofinf1o  8588  finsschain  8620  wemaplem3  8801  oemapvali  8935  iunfictbso  9328  enfin2i  9535  fin1a2s  9628  ttukeylem6  9728  distrlem4pr  10240  mulcmpblnr  10285  prsrlem1  10286  dedekind  10597  divdivdiv  11136  divmuleq  11140  divsubdiv  11151  lediv12a  11328  xralrple  12409  ssfzo12bi  12941  seqcaopr  13216  leexp2r  13347  hashbclem  13617  wrd2ind  13911  wrd2indOLD  13912  rtrclreclem3  14274  rtrclreclem4  14275  relexpindlem  14277  rtrclind  14279  rlimresb  14777  summo  14928  fsum2dlem  14979  prodmo  15144  fprod2dlem  15188  bezoutlem3  15739  bezoutlem4  15740  ncoprmgcdne1b  15844  qredeu  15852  coprmproddvdslem  15856  pcqmul  16040  pcadd  16075  pockthg  16092  prmreclem2  16103  vdwlem10  16176  ramub1lem2  16213  prmgaplem6  16242  prmgaplem7  16243  cshwsdisj  16282  mreexexlem4d  16770  mreexdomd  16772  issubc3  16971  cofucl  17010  setcmon  17199  setcepi  17200  drsdirfi  17400  poslubmo  17608  posglbmo  17609  issubmd  17811  mndind  17828  ghmpreima  18145  gaorber  18203  psgnunilem4  18381  psgneu  18390  odcau  18484  pgpssslw  18494  fislw  18505  lsmsubm  18533  efgsfo  18618  gsum2d2  18841  pgpfac1lem5  18945  pgpfac1  18946  pgpfaclem2  18948  pgpfaclem3  18949  unitgrp  19134  lmodprop2d  19412  lsspropd  19505  lbsextlem4  19649  assapropd  19815  evlslem1  20002  mdetunilem8  20926  mdetuni0  20928  mdetmul  20930  neiint  21410  restbas  21464  iscnp4  21569  cnpco  21573  nrmsep  21663  regsep2  21682  ordthauslem  21689  1stcfb  21751  1stcrest  21759  2ndcctbss  21761  2ndcdisj  21762  2ndcomap  21764  dis2ndc  21766  nlly2i  21782  islly2  21790  hausllycmp  21800  lly1stc  21802  comppfsc  21838  ptbasin  21883  txcls  21910  ptcnp  21928  txlly  21942  txnlly  21943  txtube  21946  txcmplem1  21947  txcmplem2  21948  xkococnlem  21965  basqtop  22017  regr1lem  22045  kqreglem1  22047  kqreglem2  22048  kqnrmlem1  22049  kqnrmlem2  22050  reghmph  22099  nrmhmph  22100  opnfbas  22148  rnelfmlem  22258  fmufil  22265  fclscf  22331  fclsfnflim  22333  flimfnfcls  22334  uffclsflim  22337  cnpfcfi  22346  cnpfcf  22347  alexsubALTlem2  22354  alexsubALTlem4  22356  tgpconncompeqg  22417  ghmcnp  22420  qustgplem  22426  tsmsxp  22460  blssps  22731  blss  22732  blcld  22812  metequiv2  22817  met2ndci  22829  prdsxmslem2  22836  txmetcnp  22854  nlmvscnlem1  22992  xrge0tsms  23139  ipcnlem1  23545  iscmet3  23593  metsscmetcld  23615  minveclem3  23729  pmltpc  23748  ovolscalem2  23812  ovolicc2lem5  23819  ovolicc2  23820  nulmbl2  23834  ioombl1  23860  uniioombllem6  23886  uniioombl  23887  vitalilem3  23908  i1faddlem  23991  mbfmullem  24023  itg2split  24047  lhop2  24309  dvfsumrlim  24325  itgsubst  24343  plydivex  24583  plyexmo  24599  ulmbdd  24683  cxploglim  25251  dchrptlem2  25537  lgsquad2lem2  25657  2sqlem5  25694  dchrvmasumif  25775  rpvmasum2  25784  dchrisum0re  25785  dchrisum0lem3  25791  dchrisum0  25792  dchrmusum  25796  dchrvmasum  25797  pntibndlem3  25864  pntlemp  25882  ostth3  25910  legtrid  26073  hlcgreu  26100  mirreu3  26136  midexlem  26174  opphllem  26217  mideulem  26218  opphllem1  26229  oppperpex  26235  lnperpex  26285  trgcopy  26286  iscgra1  26292  cgraswap  26302  cgracom  26304  cgratr  26305  flatcgra  26306  acopyeu  26317  ax5seglem9  26420  ax5seg  26421  axcontlem8  26454  axcontlem12  26458  clwwlknonwwlknonb  27628  2pthfrgr  27812  frgrnbnb  27821  ablo4  28098  smcnlem  28245  pjhthmo  28854  mdslmd1lem1  29877  xrge0tsmsd  30530  locfinref  30749  xpinpreima2  30794  qqhval2  30867  dya2iocnrect  31184  orvcgteel  31371  orvclteel  31376  derangenlem  32003  cnpconn  32062  txpconn  32064  connpconn  32067  pconnpi1  32069  iccllysconn  32082  rellysconn  32083  cvmcov2  32107  cvmliftmolem2  32114  cvmliftmo  32116  cvmliftlem15  32130  cvmliftpht  32150  cvmlift3lem2  32152  fpr3g  32643  nosupbnd1lem1  32729  nosupbnd2  32737  conway  32785  cgrextend  32990  btwnouttr2  33004  cgrsub  33027  cgrxfr  33037  btwnxfr  33038  colineardim1  33043  btwnconn1lem6  33074  btwnconn1lem13  33081  btwnconn1lem14  33082  btwnconn3  33085  seglecgr12im  33092  segleantisym  33097  outsideofeq  33112  outsidele  33114  lineunray  33129  linethru  33135  fnessref  33226  neibastop2lem  33229  neibastop2  33230  unblimceq0lem  33365  knoppndvlem22  33392  bj-finsumval0  34030  isbasisrelowllem1  34078  isbasisrelowllem2  34079  mblfinlem3  34372  cnambfre  34381  areacirclem5  34427  istotbnd3  34491  sstotbnd  34495  crngm4  34723  cvlcvr1  35920  4atlem12  36193  paddasslem10  36410  paddasslem12  36412  paddasslem13  36413  lhpexle3lem  36592  cdlemd4  36782  cdleme0cq  36796  cdlemefs32sn1aw  36995  cdleme43fsv1snlem  37001  cdleme32d  37025  cdleme32f  37027  cdleme40m  37048  cdleme40n  37049  cdleme42keg  37067  cdleme42mgN  37069  cdleme50trn2  37132  cdleme50trn3  37134  cdlemm10N  37699  dihvalcqpre  37816  dihopelvalcpre  37829  dihmeetlem1N  37871  dihjat1lem  38009  mapd0  38246  mapdh9a  38370  diophin  38765  pellexlem3  38824  pellexlem5  38826  pellex  38828  pell14qrmulcl  38856  jm2.19lem3  38984  jm2.25  38992  jm2.27b  38999  lmhmfgsplit  39082  hbtlem2  39120  hbtlem5  39124  gsumws3  39914  gsumws4  39915  mnuprdlem4  39986  fnchoice  40705  stoweidlem17  41733  stoweidlem53  41769  stoweidlem61  41777  qndenserrnbllem  42010  bgoldbtbnd  43342  rabsubmgmd  43426  lindslinindsimp1  43879