Theorem simprrl 793

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  prproe  4865  f1prex  7284  fpr3g  8287  fprresex  8312  nnaordex2  8632  naddssim  8679  eroveu  8817  mapdom2  9151  domunfican  9297  fofinf1o  9305  finsschain  9332  wemaplem3  9526  oemapvali  9669  iunfictbso  10174  enfin2i  10380  fin1a2s  10473  ttukeylem6  10573  distrlem4pr  11092  mulcmpblnr  11137  prsrlem1  11138  dedekind  11454  divdivdiv  11999  divmuleq  12003  divsubdiv  12014  lediv12a  12191  xralrple  13316  ssfzo12bi  13876  seqcaopr  14162  leexp2r  14297  hashbclem  14577  wrd2ind  14852  rtrclreclem3  15193  rtrclreclem4  15194  relexpindlem  15196  rtrclind  15198  rlimresb  15712  summo  15863  fsum2dlem  15916  prodmo  16083  fprod2dlem  16127  bezoutlem3  16694  bezoutlem4  16695  ncoprmgcdne1b  16805  qredeu  16813  coprmproddvdslem  16817  prmdvdsncoprmbd  16883  pcqmul  17011  pcadd  17047  pockthg  17064  prmreclem2  17075  vdwlem10  17148  ramub1lem2  17185  prmgaplem6  17214  prmgaplem7  17215  cshwsdisj  17256  mreexexlem4d  17801  mreexdomd  17803  issubc3  18004  cofucl  18043  setcmon  18242  setcepi  18243  drsdirfi  18459  poslubmo  18563  posglbmo  18564  mgmn0plusgf  18807  grprida  18836  rabsubmgmd  18873  issubmd  18981  mndind  19004  ghmpreima  19432  gaorber  19502  psgnunilem4  19691  psgneu  19700  odcau  19798  pgpssslw  19808  fislw  19819  lsmsubm  19847  efgsfo  19933  gsum2d2  20168  pgpfac1lem5  20275  pgpfac1  20276  pgpfaclem2  20278  pgpfaclem3  20279  unitgrp  20593  lmodprop2d  21179  lsspropd  21272  lbsextlem4  21419  assapropd  22159  evlslem1  22371  mdetunilem8  22914  mdetuni0  22916  mdetmul  22918  neiint  23402  restbas  23456  iscnp4  23561  cnpco  23565  nrmsep  23655  regsep2  23674  ordthauslem  23681  1stcfb  23743  1stcrest  23751  2ndcctbss  23754  2ndcdisj  23755  2ndcomap  23757  dis2ndc  23759  nlly2i  23775  islly2  23783  hausllycmp  23793  lly1stc  23795  comppfsc  23831  ptbasin  23876  txcls  23903  ptcnp  23921  txlly  23935  txnlly  23936  txtube  23939  txcmplem1  23940  txcmplem2  23941  xkococnlem  23958  basqtop  24010  regr1lem  24038  kqreglem1  24040  kqreglem2  24041  kqnrmlem1  24042  kqnrmlem2  24043  reghmph  24092  nrmhmph  24093  opnfbas  24141  rnelfmlem  24251  fmufil  24258  fclscf  24324  fclsfnflim  24326  flimfnfcls  24327  uffclsflim  24330  cnpfcfi  24339  cnpfcf  24340  alexsubALTlem2  24347  alexsubALTlem4  24349  tgpconncompeqg  24411  ghmcnp  24414  qustgplem  24420  tsmsxp  24454  blssps  24723  blss  24724  blcld  24804  metequiv2  24809  met2ndci  24821  prdsxmslem2  24828  txmetcnp  24846  nlmvscnlem1  24985  xrge0tsms  25134  ipcnlem1  25546  iscmet3  25594  metsscmetcld  25616  minveclem3  25730  pmltpc  25751  ovolscalem2  25815  ovolicc2lem5  25822  ovolicc2  25823  nulmbl2  25837  ioombl1  25863  uniioombllem6  25889  uniioombl  25890  vitalilem3  25911  i1faddlem  25994  mbfmullem  26026  itg2split  26050  lhop2  26315  dvfsumrlim  26331  itgsubst  26349  plydivex  26600  plyexmo  26618  ulmbdd  26707  cxploglim  27287  dchrptlem2  27574  lgsquad2lem2  27694  2sqlem5  27731  dchrvmasumif  27812  rpvmasum2  27821  dchrisum0re  27822  dchrisum0lem3  27828  dchrisum0  27829  dchrmusum  27833  dchrvmasum  27834  pntibndlem3  27901  pntlemp  27919  ostth3  27947  nna4b4nsq  27972  nosupbday  28044  nosupbnd1lem1  28047  nosupbnd2  28055  noinfno  28057  noinfbday  28059  noinfbnd1lem1  28062  noinfbnd2  28070  conway  28147  madebdaylemlrcut  28267  mulsproplem9  28492  mulsproplem13  28496  mulsproplem14  28497  mulsuniflem  28517  uzsind  28773  bdayfinbndlem1  28835  readdscl  28867  legtrid  29036  hlcgreu  29066  mirreu3  29108  midexlem  29146  opphllem  29193  mideulem  29194  opphllem1  29205  oppperpex  29211  lnperpex  29291  trgcopy  29293  iscgra1  29299  cgraswap  29309  cgracom  29311  cgratr  29312  flatcgra  29314  acopyeu  29324  cgrabasimass  29360  ax5seglem9  29497  ax5seg  29498  axcontlem8  29531  axcontlem12  29535  clwwlknonwwlknonb  30679  2pthfrgr  30867  frgrnbnb  30876  ablo4  31134  smcnlem  31281  pjhthmo  31886  mdslmd1lem1  32909  xrge0tsmsd  33616  locfinref  34455  xpinpreima2  34521  qqhval2  34596  dya2iocnrect  34896  orvcgteel  35083  orvclteel  35088  derangenlem  35905  cnpconn  35964  txpconn  35966  connpconn  35969  pconnpi1  35971  iccllysconn  35984  rellysconn  35985  cvmcov2  36009  cvmliftmolem2  36016  cvmliftmo  36018  cvmliftlem15  36032  cvmliftpht  36052  cvmlift3lem2  36054  cgrextend  36743  btwnouttr2  36757  cgrsub  36780  cgrxfr  36790  btwnxfr  36791  colineardim1  36796  btwnconn1lem6  36827  btwnconn1lem13  36834  btwnconn1lem14  36835  btwnconn3  36838  seglecgr12im  36845  segleantisym  36850  outsideofeq  36865  outsidele  36867  lineunray  36882  linethru  36888  fnessref  37115  neibastop2lem  37118  neibastop2  37119  weiunpo  37223  unblimceq0lem  37342  knoppndvlem22  37369  bj-finsumval0  38174  isbasisrelowllem1  38246  isbasisrelowllem2  38247  mblfinlem3  38545  cnambfre  38554  areacirclem5  38598  istotbnd3  38673  sstotbnd  38677  crngm4  38905  cvlcvr1  40364  4atlem12  40637  paddasslem10  40854  paddasslem12  40856  paddasslem13  40857  lhpexle3lem  41036  cdlemd4  41226  cdleme0cq  41240  cdlemefs32sn1aw  41439  cdleme43fsv1snlem  41445  cdleme32d  41469  cdleme32f  41471  cdleme40m  41492  cdleme40n  41493  cdleme42keg  41511  cdleme42mgN  41513  cdleme50trn2  41576  cdleme50trn3  41578  cdlemm10N  42143  dihvalcqpre  42260  dihopelvalcpre  42273  dihmeetlem1N  42315  dihjat1lem  42453  mapd0  42690  mapdh9a  42814  fsuppssind  43583  diophin  43736  pellexlem3  43791  pellexlem5  43793  pellex  43795  pell14qrmulcl  43823  jm2.19lem3  43951  jm2.25  43959  jm2.27b  43966  lmhmfgsplit  44046  hbtlem2  44084  hbtlem5  44088  gsumws3  45155  gsumws4  45156  mnuprdlem4  45218  fnchoice  45989  stoweidlem17  46971  stoweidlem53  47007  stoweidlem61  47015  qndenserrnbllem  47248  bgoldbtbnd  48851  cycldlenngric  48970  isubgr3stgrlem6  49013  lindslinindsimp1  49513  brab2dd  49882  prsthinc  50516