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  7292  fpr3g  8303  fprresex  8328  nnaordex2  8648  naddssim  8695  eroveu  8833  mapdom2  9167  domunfican  9313  fofinf1o  9321  finsschain  9348  wemaplem3  9542  oemapvali  9685  iunfictbso  10193  enfin2i  10399  fin1a2s  10492  ttukeylem6  10592  distrlem4pr  11111  mulcmpblnr  11156  prsrlem1  11157  dedekind  11473  divdivdiv  12018  divmuleq  12022  divsubdiv  12033  lediv12a  12210  xralrple  13335  ssfzo12bi  13896  seqcaopr  14182  leexp2r  14317  hashbclem  14597  wrd2ind  14872  rtrclreclem3  15213  rtrclreclem4  15214  relexpindlem  15216  rtrclind  15218  rlimresb  15732  summo  15883  fsum2dlem  15936  prodmo  16103  fprod2dlem  16147  bezoutlem3  16714  bezoutlem4  16715  ncoprmgcdne1b  16825  qredeu  16833  coprmproddvdslem  16837  prmdvdsncoprmbd  16903  pcqmul  17031  pcadd  17067  pockthg  17084  prmreclem2  17095  vdwlem10  17168  ramub1lem2  17205  prmgaplem6  17234  prmgaplem7  17235  cshwsdisj  17276  mreexexlem4d  17821  mreexdomd  17823  issubc3  18024  cofucl  18063  setcmon  18262  setcepi  18263  drsdirfi  18479  poslubmo  18583  posglbmo  18584  mgmn0plusgf  18827  grprida  18856  rabsubmgmd  18893  issubmd  19001  mndind  19024  ghmpreima  19452  gaorber  19522  psgnunilem4  19711  psgneu  19720  odcau  19818  pgpssslw  19828  fislw  19839  lsmsubm  19867  efgsfo  19953  gsum2d2  20188  pgpfac1lem5  20295  pgpfac1  20296  pgpfaclem2  20298  pgpfaclem3  20299  unitgrp  20613  lmodprop2d  21199  lsspropd  21292  lbsextlem4  21439  assapropd  22179  evlslem1  22391  mdetunilem8  22934  mdetuni0  22936  mdetmul  22938  neiint  23422  restbas  23476  iscnp4  23581  cnpco  23585  nrmsep  23675  regsep2  23694  ordthauslem  23701  1stcfb  23763  1stcrest  23771  2ndcctbss  23774  2ndcdisj  23775  2ndcomap  23777  dis2ndc  23779  nlly2i  23795  islly2  23803  hausllycmp  23813  lly1stc  23815  comppfsc  23851  ptbasin  23896  txcls  23923  ptcnp  23941  txlly  23955  txnlly  23956  txtube  23959  txcmplem1  23960  txcmplem2  23961  xkococnlem  23978  basqtop  24030  regr1lem  24058  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  reghmph  24112  nrmhmph  24113  opnfbas  24161  rnelfmlem  24271  fmufil  24278  fclscf  24344  fclsfnflim  24346  flimfnfcls  24347  uffclsflim  24350  cnpfcfi  24359  cnpfcf  24360  alexsubALTlem2  24367  alexsubALTlem4  24369  tgpconncompeqg  24431  ghmcnp  24434  qustgplem  24440  tsmsxp  24474  blssps  24743  blss  24744  blcld  24824  metequiv2  24829  met2ndci  24841  prdsxmslem2  24848  txmetcnp  24866  nlmvscnlem1  25005  xrge0tsms  25154  ipcnlem1  25566  iscmet3  25614  metsscmetcld  25636  minveclem3  25750  pmltpc  25771  ovolscalem2  25835  ovolicc2lem5  25842  ovolicc2  25843  nulmbl2  25857  ioombl1  25883  uniioombllem6  25909  uniioombl  25910  vitalilem3  25931  i1faddlem  26014  mbfmullem  26046  itg2split  26070  lhop2  26335  dvfsumrlim  26351  itgsubst  26369  plydivex  26618  plyexmo  26636  ulmbdd  26725  cxploglim  27305  dchrptlem2  27592  lgsquad2lem2  27712  2sqlem5  27749  dchrvmasumif  27830  rpvmasum2  27839  dchrisum0re  27840  dchrisum0lem3  27846  dchrisum0  27847  dchrmusum  27851  dchrvmasum  27852  pntibndlem3  27919  pntlemp  27937  ostth3  27965  nna4b4nsq  27990  nosupbday  28062  nosupbnd1lem1  28065  nosupbnd2  28073  noinfno  28075  noinfbday  28077  noinfbnd1lem1  28080  noinfbnd2  28088  conway  28165  madebdaylemlrcut  28285  mulsproplem9  28510  mulsproplem13  28514  mulsproplem14  28515  mulsuniflem  28535  uzsind  28791  bdayfinbndlem1  28853  readdscl  28885  legtrid  29054  hlcgreu  29084  mirreu3  29126  midexlem  29164  opphllem  29211  mideulem  29212  opphllem1  29223  oppperpex  29229  lnperpex  29309  trgcopy  29311  iscgra1  29317  cgraswap  29327  cgracom  29329  cgratr  29330  flatcgra  29332  acopyeu  29342  cgrabasimass  29378  ax5seglem9  29515  ax5seg  29516  axcontlem8  29549  axcontlem12  29553  clwwlknonwwlknonb  30697  2pthfrgr  30885  frgrnbnb  30894  ablo4  31152  smcnlem  31299  pjhthmo  31904  mdslmd1lem1  32927  xrge0tsmsd  33634  locfinref  34473  xpinpreima2  34539  qqhval2  34614  dya2iocnrect  34913  orvcgteel  35100  orvclteel  35105  derangenlem  35936  cnpconn  35995  txpconn  35997  connpconn  36000  pconnpi1  36002  iccllysconn  36015  rellysconn  36016  cvmcov2  36040  cvmliftmolem2  36047  cvmliftmo  36049  cvmliftlem15  36063  cvmliftpht  36083  cvmlift3lem2  36085  cgrextend  36773  btwnouttr2  36787  cgrsub  36810  cgrxfr  36820  btwnxfr  36821  colineardim1  36826  btwnconn1lem6  36857  btwnconn1lem13  36864  btwnconn1lem14  36865  btwnconn3  36868  seglecgr12im  36875  segleantisym  36880  outsideofeq  36895  outsidele  36897  lineunray  36912  linethru  36918  fnessref  37145  neibastop2lem  37148  neibastop2  37149  weiunpo  37253  unblimceq0lem  37372  knoppndvlem22  37399  bj-finsumval0  38206  isbasisrelowllem1  38278  isbasisrelowllem2  38279  mblfinlem3  38577  cnambfre  38586  areacirclem5  38630  istotbnd3  38705  sstotbnd  38709  crngm4  38937  cvlcvr1  40396  4atlem12  40669  paddasslem10  40886  paddasslem12  40888  paddasslem13  40889  lhpexle3lem  41068  cdlemd4  41258  cdleme0cq  41272  cdlemefs32sn1aw  41471  cdleme43fsv1snlem  41477  cdleme32d  41501  cdleme32f  41503  cdleme40m  41524  cdleme40n  41525  cdleme42keg  41543  cdleme42mgN  41545  cdleme50trn2  41608  cdleme50trn3  41610  cdlemm10N  42175  dihvalcqpre  42292  dihopelvalcpre  42305  dihmeetlem1N  42347  dihjat1lem  42485  mapd0  42722  mapdh9a  42846  fsuppssind  43621  diophin  43782  pellexlem3  43837  pellexlem5  43839  pellex  43841  pell14qrmulcl  43869  jm2.19lem3  43997  jm2.25  44005  jm2.27b  44012  lmhmfgsplit  44087  hbtlem2  44125  hbtlem5  44129  gsumws3  45195  gsumws4  45196  mnuprdlem4  45258  fnchoice  46045  stoweidlem17  47026  stoweidlem53  47062  stoweidlem61  47070  qndenserrnbllem  47303  bgoldbtbnd  48906  cycldlenngric  49025  isubgr3stgrlem6  49068  lindslinindsimp1  49568  brab2dd  49937  prsthinc  50571