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  4836  f1prex  7318  fpr3g  8334  fprresex  8359  nnaordex2  8679  naddssim  8726  eroveu  8864  mapdom2  9198  domunfican  9344  fofinf1o  9352  finsschain  9379  wemaplem3  9572  oemapvali  9715  iunfictbso  10223  enfin2i  10429  fin1a2s  10522  ttukeylem6  10622  distrlem4pr  11141  mulcmpblnr  11186  prsrlem1  11187  dedekind  11503  divdivdiv  12048  divmuleq  12052  divsubdiv  12063  lediv12a  12240  xralrple  13365  ssfzo12bi  13926  seqcaopr  14212  leexp2r  14347  hashbclem  14627  wrd2ind  14903  rtrclreclem3  15245  rtrclreclem4  15246  relexpindlem  15248  rtrclind  15250  rlimresb  15764  summo  15915  fsum2dlem  15968  prodmo  16135  fprod2dlem  16179  bezoutlem3  16746  bezoutlem4  16747  ncoprmgcdne1b  16857  qredeu  16865  coprmproddvdslem  16869  prmdvdsncoprmbd  16935  pcqmul  17063  pcadd  17099  pockthg  17116  prmreclem2  17127  vdwlem10  17200  ramub1lem2  17237  prmgaplem6  17266  prmgaplem7  17267  cshwsdisj  17308  mreexexlem4d  17853  mreexdomd  17855  issubc3  18056  cofucl  18095  setcmon  18294  setcepi  18295  drsdirfi  18511  poslubmo  18615  posglbmo  18616  mgmn0plusgf  18859  grprida  18888  rabsubmgmd  18925  issubmd  19033  mndind  19056  ghmpreima  19484  gaorber  19555  psgnunilem4  19744  psgneu  19753  odcau  19851  pgpssslw  19861  fislw  19872  lsmsubm  19900  efgsfo  19986  gsum2d2  20221  pgpfac1lem5  20328  pgpfac1  20329  pgpfaclem2  20331  pgpfaclem3  20332  unitgrp  20646  lmodprop2d  21232  lsspropd  21325  lbsextlem4  21472  assapropd  22212  evlslem1  22424  mdetunilem8  22967  mdetuni0  22969  mdetmul  22971  neiint  23455  restbas  23509  iscnp4  23614  cnpco  23618  nrmsep  23708  regsep2  23727  ordthauslem  23734  1stcfb  23796  1stcrest  23804  2ndcctbss  23807  2ndcdisj  23808  2ndcomap  23810  dis2ndc  23812  nlly2i  23828  islly2  23836  hausllycmp  23846  lly1stc  23848  comppfsc  23884  ptbasin  23929  txcls  23956  ptcnp  23974  txlly  23988  txnlly  23989  txtube  23992  txcmplem1  23993  txcmplem2  23994  xkococnlem  24011  basqtop  24063  regr1lem  24091  kqreglem1  24093  kqreglem2  24094  kqnrmlem1  24095  kqnrmlem2  24096  reghmph  24145  nrmhmph  24146  opnfbas  24194  rnelfmlem  24304  fmufil  24311  fclscf  24377  fclsfnflim  24379  flimfnfcls  24380  uffclsflim  24383  cnpfcfi  24392  cnpfcf  24393  alexsubALTlem2  24400  alexsubALTlem4  24402  tgpconncompeqg  24464  ghmcnp  24467  qustgplem  24473  tsmsxp  24507  blssps  24776  blss  24777  blcld  24857  metequiv2  24862  met2ndci  24874  prdsxmslem2  24881  txmetcnp  24899  nlmvscnlem1  25038  xrge0tsms  25187  ipcnlem1  25599  iscmet3  25647  metsscmetcld  25669  minveclem3  25783  pmltpc  25804  ovolscalem2  25868  ovolicc2lem5  25875  ovolicc2  25876  nulmbl2  25890  ioombl1  25916  uniioombllem6  25942  uniioombl  25943  vitalilem3  25964  i1faddlem  26047  mbfmullem  26079  itg2split  26103  lhop2  26368  dvfsumrlim  26384  itgsubst  26402  plydivex  26651  plyexmo  26669  ulmbdd  26758  cxploglim  27338  dchrptlem2  27625  lgsquad2lem2  27745  2sqlem5  27782  dchrvmasumif  27863  rpvmasum2  27872  dchrisum0re  27873  dchrisum0lem3  27879  dchrisum0  27880  dchrmusum  27884  dchrvmasum  27885  pntibndlem3  27952  pntlemp  27970  ostth3  27998  nna4b4nsq  28023  nosupbday  28095  nosupbnd1lem1  28098  nosupbnd2  28106  noinfno  28108  noinfbday  28110  noinfbnd1lem1  28113  noinfbnd2  28121  conway  28198  madebdaylemlrcut  28318  mulsproplem9  28543  mulsproplem13  28547  mulsproplem14  28548  mulsuniflem  28568  uzsind  28824  bdayfinbndlem1  28886  readdscl  28918  legtrid  29087  hlcgreu  29117  mirreu3  29159  midexlem  29197  opphllem  29244  mideulem  29245  opphllem1  29256  oppperpex  29262  lnperpex  29342  trgcopy  29344  iscgra1  29350  cgraswap  29360  cgracom  29362  cgratr  29363  flatcgra  29365  acopyeu  29375  cgrabasimass  29411  ax5seglem9  29548  ax5seg  29549  axcontlem8  29582  axcontlem12  29586  clwwlknonwwlknonb  30730  2pthfrgr  30918  frgrnbnb  30927  ablo4  31185  smcnlem  31332  pjhthmo  31937  mdslmd1lem1  32960  tgextahp  33106  xrge0tsmsd  33710  locfinref  34556  xpinpreima2  34622  qqhval2  34697  dya2iocnrect  34996  orvcgteel  35183  orvclteel  35188  derangenlem  36116  cnpconn  36175  txpconn  36177  connpconn  36180  pconnpi1  36182  iccllysconn  36195  rellysconn  36196  cvmcov2  36220  cvmliftmolem2  36227  cvmliftmo  36229  cvmliftlem15  36243  cvmliftpht  36263  cvmlift3lem2  36265  cgrextend  36964  btwnouttr2  36978  cgrsub  37001  cgrxfr  37011  btwnxfr  37012  colineardim1  37017  btwnconn1lem6  37048  btwnconn1lem13  37055  btwnconn1lem14  37056  btwnconn3  37059  seglecgr12im  37066  segleantisym  37071  outsideofeq  37086  outsidele  37088  lineunray  37103  linethru  37109  fnessref  37336  neibastop2lem  37339  neibastop2  37340  weiunpo  37444  unblimceq0lem  37563  knoppndvlem22  37590  bj-finsumval0  38411  isbasisrelowllem1  38483  isbasisrelowllem2  38484  mblfinlem3  38782  cnambfre  38791  areacirclem5  38835  istotbnd3  38908  sstotbnd  38912  crngm4  39140  cvlcvr1  40599  4atlem12  40872  paddasslem10  41089  paddasslem12  41091  paddasslem13  41092  lhpexle3lem  41271  cdlemd4  41461  cdleme0cq  41475  cdlemefs32sn1aw  41674  cdleme43fsv1snlem  41680  cdleme32d  41704  cdleme32f  41706  cdleme40m  41727  cdleme40n  41728  cdleme42keg  41746  cdleme42mgN  41748  cdleme50trn2  41811  cdleme50trn3  41813  cdlemm10N  42378  dihvalcqpre  42495  dihopelvalcpre  42508  dihmeetlem1N  42550  dihjat1lem  42688  mapd0  42925  mapdh9a  43049  fsuppssind  43825  diophin  43987  pellexlem3  44042  pellexlem5  44044  pellex  44046  pell14qrmulcl  44074  jm2.19lem3  44202  jm2.25  44210  jm2.27b  44217  lmhmfgsplit  44292  hbtlem2  44329  hbtlem5  44333  gsumws3  45399  gsumws4  45400  mnuprdlem4  45462  fnchoice  46262  stoweidlem17  47242  stoweidlem53  47278  stoweidlem61  47286  qndenserrnbllem  47519  bgoldbtbnd  49122  cycldlenngric  49241  isubgr3stgrlem6  49284  lindslinindsimp1  49784  brab2dd  50154  prsthinc  50814  parmapcl2  50985