Theorem simprrl 779

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  prproe  4842  f1prex  7188  fpr3g  8132  fprresex  8157  wfrlem17OLD  8187  eroveu  8632  undomOLD  8885  mapdom2  8973  domunfican  9131  fofinf1o  9138  finsschain  9170  wemaplem3  9351  oemapvali  9486  iunfictbso  9916  enfin2i  10123  fin1a2s  10216  ttukeylem6  10316  distrlem4pr  10828  mulcmpblnr  10873  prsrlem1  10874  dedekind  11184  divdivdiv  11722  divmuleq  11726  divsubdiv  11737  lediv12a  11914  xralrple  12985  ssfzo12bi  13528  seqcaopr  13806  leexp2r  13938  hashbclem  14209  wrd2ind  14481  rtrclreclem3  14816  rtrclreclem4  14817  relexpindlem  14819  rtrclind  14821  rlimresb  15319  summo  15474  fsum2dlem  15527  prodmo  15691  fprod2dlem  15735  bezoutlem3  16294  bezoutlem4  16295  ncoprmgcdne1b  16400  qredeu  16408  coprmproddvdslem  16412  prmdvdsncoprmbd  16476  pcqmul  16599  pcadd  16635  pockthg  16652  prmreclem2  16663  vdwlem10  16736  ramub1lem2  16773  prmgaplem6  16802  prmgaplem7  16803  cshwsdisj  16845  mreexexlem4d  17401  mreexdomd  17403  issubc3  17609  cofucl  17648  setcmon  17847  setcepi  17848  drsdirfi  18068  poslubmo  18174  posglbmo  18175  grpridd  18404  issubmd  18490  mndind  18511  ghmpreima  18901  gaorber  18959  psgnunilem4  19150  psgneu  19159  odcau  19254  pgpssslw  19264  fislw  19275  lsmsubm  19303  efgsfo  19390  gsum2d2  19620  pgpfac1lem5  19727  pgpfac1  19728  pgpfaclem2  19730  pgpfaclem3  19731  unitgrp  19954  lmodprop2d  20230  lsspropd  20324  lbsextlem4  20468  assapropd  21121  evlslem1  21337  mdetunilem8  21813  mdetuni0  21815  mdetmul  21817  neiint  22300  restbas  22354  iscnp4  22459  cnpco  22463  nrmsep  22553  regsep2  22572  ordthauslem  22579  1stcfb  22641  1stcrest  22649  2ndcctbss  22651  2ndcdisj  22652  2ndcomap  22654  dis2ndc  22656  nlly2i  22672  islly2  22680  hausllycmp  22690  lly1stc  22692  comppfsc  22728  ptbasin  22773  txcls  22800  ptcnp  22818  txlly  22832  txnlly  22833  txtube  22836  txcmplem1  22837  txcmplem2  22838  xkococnlem  22855  basqtop  22907  regr1lem  22935  kqreglem1  22937  kqreglem2  22938  kqnrmlem1  22939  kqnrmlem2  22940  reghmph  22989  nrmhmph  22990  opnfbas  23038  rnelfmlem  23148  fmufil  23155  fclscf  23221  fclsfnflim  23223  flimfnfcls  23224  uffclsflim  23227  cnpfcfi  23236  cnpfcf  23237  alexsubALTlem2  23244  alexsubALTlem4  23246  tgpconncompeqg  23308  ghmcnp  23311  qustgplem  23317  tsmsxp  23351  blssps  23622  blss  23623  blcld  23706  metequiv2  23711  met2ndci  23723  prdsxmslem2  23730  txmetcnp  23748  nlmvscnlem1  23895  xrge0tsms  24042  ipcnlem1  24454  iscmet3  24502  metsscmetcld  24524  minveclem3  24638  pmltpc  24659  ovolscalem2  24723  ovolicc2lem5  24730  ovolicc2  24731  nulmbl2  24745  ioombl1  24771  uniioombllem6  24797  uniioombl  24798  vitalilem3  24819  i1faddlem  24902  mbfmullem  24935  itg2split  24959  lhop2  25224  dvfsumrlim  25240  itgsubst  25258  plydivex  25502  plyexmo  25518  ulmbdd  25602  cxploglim  26172  dchrptlem2  26458  lgsquad2lem2  26578  2sqlem5  26615  dchrvmasumif  26696  rpvmasum2  26705  dchrisum0re  26706  dchrisum0lem3  26712  dchrisum0  26713  dchrmusum  26717  dchrvmasum  26718  pntibndlem3  26785  pntlemp  26803  ostth3  26831  legtrid  26997  hlcgreu  27024  mirreu3  27060  midexlem  27098  opphllem  27141  mideulem  27142  opphllem1  27153  oppperpex  27159  lnperpex  27209  trgcopy  27210  iscgra1  27216  cgraswap  27226  cgracom  27228  cgratr  27229  flatcgra  27230  acopyeu  27240  ax5seglem9  27350  ax5seg  27351  axcontlem8  27384  axcontlem12  27388  clwwlknonwwlknonb  28515  2pthfrgr  28693  frgrnbnb  28702  ablo4  28957  smcnlem  29104  pjhthmo  29709  mdslmd1lem1  30732  xrge0tsmsd  31362  locfinref  31836  xpinpreima2  31902  qqhval2  31977  dya2iocnrect  32293  orvcgteel  32479  orvclteel  32484  derangenlem  33178  cnpconn  33237  txpconn  33239  connpconn  33242  pconnpi1  33244  iccllysconn  33257  rellysconn  33258  cvmcov2  33282  cvmliftmolem2  33289  cvmliftmo  33291  cvmliftlem15  33305  cvmliftpht  33325  cvmlift3lem2  33327  naddssim  33882  nosupbday  33953  nosupbnd1lem1  33956  nosupbnd2  33964  noinfno  33966  noinfbday  33968  noinfbnd1lem1  33971  noinfbnd2  33979  conway  34038  madebdaylemlrcut  34124  cgrextend  34355  btwnouttr2  34369  cgrsub  34392  cgrxfr  34402  btwnxfr  34403  colineardim1  34408  btwnconn1lem6  34439  btwnconn1lem13  34446  btwnconn1lem14  34447  btwnconn3  34450  seglecgr12im  34457  segleantisym  34462  outsideofeq  34477  outsidele  34479  lineunray  34494  linethru  34500  fnessref  34591  neibastop2lem  34594  neibastop2  34595  unblimceq0lem  34731  knoppndvlem22  34758  bj-finsumval0  35500  isbasisrelowllem1  35570  isbasisrelowllem2  35571  mblfinlem3  35860  cnambfre  35869  areacirclem5  35913  istotbnd3  35973  sstotbnd  35977  crngm4  36205  cvlcvr1  37395  4atlem12  37668  paddasslem10  37885  paddasslem12  37887  paddasslem13  37888  lhpexle3lem  38067  cdlemd4  38257  cdleme0cq  38271  cdlemefs32sn1aw  38470  cdleme43fsv1snlem  38476  cdleme32d  38500  cdleme32f  38502  cdleme40m  38523  cdleme40n  38524  cdleme42keg  38542  cdleme42mgN  38544  cdleme50trn2  38607  cdleme50trn3  38609  cdlemm10N  39174  dihvalcqpre  39291  dihopelvalcpre  39304  dihmeetlem1N  39346  dihjat1lem  39484  mapd0  39721  mapdh9a  39845  fsuppssind  40319  nna4b4nsq  40534  diophin  40631  pellexlem3  40690  pellexlem5  40692  pellex  40694  pell14qrmulcl  40722  jm2.19lem3  40851  jm2.25  40859  jm2.27b  40866  lmhmfgsplit  40949  hbtlem2  40987  hbtlem5  40991  gsumws3  41845  gsumws4  41846  mnuprdlem4  41931  fnchoice  42610  stoweidlem17  43607  stoweidlem53  43643  stoweidlem61  43651  qndenserrnbllem  43884  bgoldbtbnd  45319  rabsubmgmd  45403  lindslinindsimp1  45856  prsthinc  46393