Theorem simprrl 792

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  prproe  4871  f1prex  7284  fpr3g  8283  fprresex  8308  nnaordex2  8626  naddssim  8673  eroveu  8811  mapdom2  9137  domunfican  9282  fofinf1o  9290  finsschain  9317  wemaplem3  9511  oemapvali  9654  iunfictbso  10099  enfin2i  10306  fin1a2s  10399  ttukeylem6  10499  distrlem4pr  11012  mulcmpblnr  11057  prsrlem1  11058  dedekind  11374  divdivdiv  11917  divmuleq  11921  divsubdiv  11932  lediv12a  12109  xralrple  13232  ssfzo12bi  13792  seqcaopr  14077  leexp2r  14212  hashbclem  14491  wrd2ind  14762  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  rlimresb  15618  summo  15770  fsum2dlem  15823  prodmo  15992  fprod2dlem  16036  bezoutlem3  16600  bezoutlem4  16601  ncoprmgcdne1b  16709  qredeu  16717  coprmproddvdslem  16721  prmdvdsncoprmbd  16787  pcqmul  16914  pcadd  16950  pockthg  16967  prmreclem2  16978  vdwlem10  17051  ramub1lem2  17088  prmgaplem6  17117  prmgaplem7  17118  cshwsdisj  17159  mreexexlem4d  17704  mreexdomd  17706  issubc3  17907  cofucl  17946  setcmon  18145  setcepi  18146  drsdirfi  18362  poslubmo  18466  posglbmo  18467  grprida  18734  rabsubmgmd  18763  issubmd  18865  mndind  18888  ghmpreima  19309  gaorber  19379  psgnunilem4  19568  psgneu  19577  odcau  19675  pgpssslw  19685  fislw  19696  lsmsubm  19724  efgsfo  19810  gsum2d2  20045  pgpfac1lem5  20152  pgpfac1  20153  pgpfaclem2  20155  pgpfaclem3  20156  unitgrp  20466  lmodprop2d  21026  lsspropd  21119  lbsextlem4  21266  assapropd  22002  evlslem1  22214  mdetunilem8  22757  mdetuni0  22759  mdetmul  22761  neiint  23242  restbas  23296  iscnp4  23401  cnpco  23405  nrmsep  23495  regsep2  23514  ordthauslem  23521  1stcfb  23583  1stcrest  23591  2ndcctbss  23593  2ndcdisj  23594  2ndcomap  23596  dis2ndc  23598  nlly2i  23614  islly2  23622  hausllycmp  23632  lly1stc  23634  comppfsc  23670  ptbasin  23715  txcls  23742  ptcnp  23760  txlly  23774  txnlly  23775  txtube  23778  txcmplem1  23779  txcmplem2  23780  xkococnlem  23797  basqtop  23849  regr1lem  23877  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  reghmph  23931  nrmhmph  23932  opnfbas  23980  rnelfmlem  24090  fmufil  24097  fclscf  24163  fclsfnflim  24165  flimfnfcls  24166  uffclsflim  24169  cnpfcfi  24178  cnpfcf  24179  alexsubALTlem2  24186  alexsubALTlem4  24188  tgpconncompeqg  24250  ghmcnp  24253  qustgplem  24259  tsmsxp  24293  blssps  24562  blss  24563  blcld  24643  metequiv2  24648  met2ndci  24660  prdsxmslem2  24667  txmetcnp  24685  nlmvscnlem1  24824  xrge0tsms  24973  ipcnlem1  25385  iscmet3  25433  metsscmetcld  25455  minveclem3  25569  pmltpc  25590  ovolscalem2  25654  ovolicc2lem5  25661  ovolicc2  25662  nulmbl2  25676  ioombl1  25702  uniioombllem6  25728  uniioombl  25729  vitalilem3  25750  i1faddlem  25833  mbfmullem  25865  itg2split  25889  lhop2  26155  dvfsumrlim  26171  itgsubst  26189  plydivex  26439  plyexmo  26455  ulmbdd  26539  cxploglim  27120  dchrptlem2  27407  lgsquad2lem2  27527  2sqlem5  27564  dchrvmasumif  27645  rpvmasum2  27654  dchrisum0re  27655  dchrisum0lem3  27661  dchrisum0  27662  dchrmusum  27666  dchrvmasum  27667  pntibndlem3  27734  pntlemp  27752  ostth3  27780  nosupbday  27847  nosupbnd1lem1  27850  nosupbnd2  27858  noinfno  27860  noinfbday  27862  noinfbnd1lem1  27865  noinfbnd2  27873  conway  27950  madebdaylemlrcut  28070  mulsproplem9  28295  mulsproplem13  28299  mulsproplem14  28300  mulsuniflem  28320  uzsind  28576  bdayfinbndlem1  28638  readdscl  28670  legtrid  28838  hlcgreu  28868  mirreu3  28909  midexlem  28947  opphllem  28994  mideulem  28995  opphllem1  29006  oppperpex  29012  lnperpex  29091  trgcopy  29093  iscgra1  29099  cgraswap  29109  cgracom  29111  cgratr  29112  flatcgra  29113  acopyeu  29123  ax5seglem9  29265  ax5seg  29266  axcontlem8  29299  axcontlem12  29303  clwwlknonwwlknonb  30435  2pthfrgr  30613  frgrnbnb  30622  ablo4  30880  smcnlem  31027  pjhthmo  31632  mdslmd1lem1  32655  xrge0tsmsd  33371  locfinref  34209  xpinpreima2  34275  qqhval2  34350  dya2iocnrect  34649  orvcgteel  34836  orvclteel  34841  derangenlem  35641  cnpconn  35700  txpconn  35702  connpconn  35705  pconnpi1  35707  iccllysconn  35720  rellysconn  35721  cvmcov2  35745  cvmliftmolem2  35752  cvmliftmo  35754  cvmliftlem15  35768  cvmliftpht  35788  cvmlift3lem2  35790  cgrextend  36478  btwnouttr2  36492  cgrsub  36515  cgrxfr  36525  btwnxfr  36526  colineardim1  36531  btwnconn1lem6  36562  btwnconn1lem13  36569  btwnconn1lem14  36570  btwnconn3  36573  seglecgr12im  36580  segleantisym  36585  outsideofeq  36600  outsidele  36602  lineunray  36617  linethru  36623  fnessref  36846  neibastop2lem  36849  neibastop2  36850  weiunpo  36954  unblimceq0lem  37073  knoppndvlem22  37100  bj-finsumval0  37907  isbasisrelowllem1  37979  isbasisrelowllem2  37980  mblfinlem3  38288  cnambfre  38297  areacirclem5  38341  istotbnd3  38400  sstotbnd  38404  crngm4  38632  cvlcvr1  40091  4atlem12  40364  paddasslem10  40581  paddasslem12  40583  paddasslem13  40584  lhpexle3lem  40763  cdlemd4  40953  cdleme0cq  40967  cdlemefs32sn1aw  41166  cdleme43fsv1snlem  41172  cdleme32d  41196  cdleme32f  41198  cdleme40m  41219  cdleme40n  41220  cdleme42keg  41238  cdleme42mgN  41240  cdleme50trn2  41303  cdleme50trn3  41305  cdlemm10N  41870  dihvalcqpre  41987  dihopelvalcpre  42000  dihmeetlem1N  42042  dihjat1lem  42180  mapd0  42417  mapdh9a  42541  fsuppssind  43305  nna4b4nsq  43372  diophin  43483  pellexlem3  43538  pellexlem5  43540  pellex  43542  pell14qrmulcl  43570  jm2.19lem3  43698  jm2.25  43706  jm2.27b  43713  lmhmfgsplit  43793  hbtlem2  43831  hbtlem5  43835  gsumws3  44902  gsumws4  44903  mnuprdlem4  44965  fnchoice  45729  stoweidlem17  46711  stoweidlem53  46747  stoweidlem61  46755  qndenserrnbllem  46988  bgoldbtbnd  48551  cycldlenngric  48670  isubgr3stgrlem6  48713  lindslinindsimp1  49214  brab2dd  49583  prsthinc  50219