Theorem simprrl 790

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  prproe  4862  f1prex  7264  fpr3g  8261  fprresex  8286  nnaordex2  8604  naddssim  8651  eroveu  8789  mapdom2  9116  domunfican  9262  fofinf1o  9272  finsschain  9299  wemaplem3  9493  oemapvali  9636  iunfictbso  10067  enfin2i  10275  fin1a2s  10368  ttukeylem6  10468  distrlem4pr  10981  mulcmpblnr  11026  prsrlem1  11027  dedekind  11343  divdivdiv  11889  divmuleq  11893  divsubdiv  11904  lediv12a  12082  xralrple  13205  ssfzo12bi  13764  seqcaopr  14049  leexp2r  14184  hashbclem  14462  wrd2ind  14733  rtrclreclem3  15070  rtrclreclem4  15071  relexpindlem  15073  rtrclind  15075  rlimresb  15575  summo  15727  fsum2dlem  15780  prodmo  15949  fprod2dlem  15993  bezoutlem3  16558  bezoutlem4  16559  ncoprmgcdne1b  16667  qredeu  16675  coprmproddvdslem  16679  prmdvdsncoprmbd  16745  pcqmul  16872  pcadd  16908  pockthg  16925  prmreclem2  16936  vdwlem10  17009  ramub1lem2  17046  prmgaplem6  17075  prmgaplem7  17076  cshwsdisj  17117  mreexexlem4d  17662  mreexdomd  17664  issubc3  17865  cofucl  17904  setcmon  18103  setcepi  18104  drsdirfi  18320  poslubmo  18424  posglbmo  18425  grprida  18692  rabsubmgmd  18721  issubmd  18823  mndind  18845  ghmpreima  19261  gaorber  19331  psgnunilem4  19520  psgneu  19529  odcau  19627  pgpssslw  19637  fislw  19648  lsmsubm  19676  efgsfo  19762  gsum2d2  19997  pgpfac1lem5  20104  pgpfac1  20105  pgpfaclem2  20107  pgpfaclem3  20108  unitgrp  20411  lmodprop2d  20971  lsspropd  21064  lbsextlem4  21211  assapropd  21903  evlslem1  22115  mdetunilem8  22659  mdetuni0  22661  mdetmul  22663  neiint  23144  restbas  23198  iscnp4  23303  cnpco  23307  nrmsep  23397  regsep2  23416  ordthauslem  23423  1stcfb  23485  1stcrest  23493  2ndcctbss  23495  2ndcdisj  23496  2ndcomap  23498  dis2ndc  23500  nlly2i  23516  islly2  23524  hausllycmp  23534  lly1stc  23536  comppfsc  23572  ptbasin  23617  txcls  23644  ptcnp  23662  txlly  23676  txnlly  23677  txtube  23680  txcmplem1  23681  txcmplem2  23682  xkococnlem  23699  basqtop  23751  regr1lem  23779  kqreglem1  23781  kqreglem2  23782  kqnrmlem1  23783  kqnrmlem2  23784  reghmph  23833  nrmhmph  23834  opnfbas  23882  rnelfmlem  23992  fmufil  23999  fclscf  24065  fclsfnflim  24067  flimfnfcls  24068  uffclsflim  24071  cnpfcfi  24080  cnpfcf  24081  alexsubALTlem2  24088  alexsubALTlem4  24090  tgpconncompeqg  24152  ghmcnp  24155  qustgplem  24161  tsmsxp  24195  blssps  24464  blss  24465  blcld  24545  metequiv2  24550  met2ndci  24562  prdsxmslem2  24569  txmetcnp  24587  nlmvscnlem1  24726  xrge0tsms  24875  ipcnlem1  25287  iscmet3  25335  metsscmetcld  25357  minveclem3  25471  pmltpc  25492  ovolscalem2  25556  ovolicc2lem5  25563  ovolicc2  25564  nulmbl2  25578  ioombl1  25604  uniioombllem6  25630  uniioombl  25631  vitalilem3  25652  i1faddlem  25735  mbfmullem  25767  itg2split  25791  lhop2  26057  dvfsumrlim  26073  itgsubst  26091  plydivex  26338  plyexmo  26354  ulmbdd  26438  cxploglim  27019  dchrptlem2  27306  lgsquad2lem2  27426  2sqlem5  27463  dchrvmasumif  27544  rpvmasum2  27553  dchrisum0re  27554  dchrisum0lem3  27560  dchrisum0  27561  dchrmusum  27565  dchrvmasum  27566  pntibndlem3  27633  pntlemp  27651  ostth3  27679  nosupbday  27746  nosupbnd1lem1  27749  nosupbnd2  27757  noinfno  27759  noinfbday  27761  noinfbnd1lem1  27764  noinfbnd2  27772  conway  27849  madebdaylemlrcut  27969  mulsproplem9  28194  mulsproplem13  28198  mulsproplem14  28199  mulsuniflem  28219  uzsind  28475  bdayfinbndlem1  28537  readdscl  28569  legtrid  28737  hlcgreu  28764  mirreu3  28800  midexlem  28838  opphllem  28881  mideulem  28882  opphllem1  28893  oppperpex  28899  lnperpex  28949  trgcopy  28950  iscgra1  28956  cgraswap  28966  cgracom  28968  cgratr  28969  flatcgra  28970  acopyeu  28980  ax5seglem9  29084  ax5seg  29085  axcontlem8  29118  axcontlem12  29122  clwwlknonwwlknonb  30254  2pthfrgr  30432  frgrnbnb  30441  ablo4  30699  smcnlem  30846  pjhthmo  31451  mdslmd1lem1  32474  xrge0tsmsd  33214  locfinref  34099  xpinpreima2  34165  qqhval2  34240  dya2iocnrect  34539  orvcgteel  34726  orvclteel  34731  derangenlem  35485  cnpconn  35544  txpconn  35546  connpconn  35549  pconnpi1  35551  iccllysconn  35564  rellysconn  35565  cvmcov2  35589  cvmliftmolem2  35596  cvmliftmo  35598  cvmliftlem15  35612  cvmliftpht  35632  cvmlift3lem2  35634  cgrextend  36322  btwnouttr2  36336  cgrsub  36359  cgrxfr  36369  btwnxfr  36370  colineardim1  36375  btwnconn1lem6  36406  btwnconn1lem13  36413  btwnconn1lem14  36414  btwnconn3  36417  seglecgr12im  36424  segleantisym  36429  outsideofeq  36444  outsidele  36446  lineunray  36461  linethru  36467  fnessref  36681  neibastop2lem  36684  neibastop2  36685  weiunpo  36789  unblimceq0lem  36908  knoppndvlem22  36935  bj-finsumval0  37741  isbasisrelowllem1  37813  isbasisrelowllem2  37814  mblfinlem3  38122  cnambfre  38131  areacirclem5  38175  istotbnd3  38234  sstotbnd  38238  crngm4  38466  cvlcvr1  39927  4atlem12  40200  paddasslem10  40417  paddasslem12  40419  paddasslem13  40420  lhpexle3lem  40599  cdlemd4  40789  cdleme0cq  40803  cdlemefs32sn1aw  41002  cdleme43fsv1snlem  41008  cdleme32d  41032  cdleme32f  41034  cdleme40m  41055  cdleme40n  41056  cdleme42keg  41074  cdleme42mgN  41076  cdleme50trn2  41139  cdleme50trn3  41141  cdlemm10N  41706  dihvalcqpre  41823  dihopelvalcpre  41836  dihmeetlem1N  41878  dihjat1lem  42016  mapd0  42253  mapdh9a  42377  fsuppssind  43139  nna4b4nsq  43206  diophin  43317  pellexlem3  43372  pellexlem5  43374  pellex  43376  pell14qrmulcl  43404  jm2.19lem3  43532  jm2.25  43540  jm2.27b  43547  lmhmfgsplit  43627  hbtlem2  43665  hbtlem5  43669  gsumws3  44736  gsumws4  44737  mnuprdlem4  44815  fnchoice  45573  stoweidlem17  46555  stoweidlem53  46591  stoweidlem61  46599  qndenserrnbllem  46832  bgoldbtbnd  48395  cycldlenngric  48514  isubgr3stgrlem6  48557  lindslinindsimp1  49043  brab2dd  49413  prsthinc  50049