Theorem simprrl 778

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  prproe  4843  f1prex  7152  fpr3g  8092  fprresex  8117  wfrlem17OLD  8147  eroveu  8584  undom  8829  mapdom2  8917  domunfican  9065  fofinf1o  9072  finsschain  9104  wemaplem3  9285  oemapvali  9420  iunfictbso  9871  enfin2i  10078  fin1a2s  10171  ttukeylem6  10271  distrlem4pr  10783  mulcmpblnr  10828  prsrlem1  10829  dedekind  11138  divdivdiv  11676  divmuleq  11680  divsubdiv  11691  lediv12a  11868  xralrple  12938  ssfzo12bi  13480  seqcaopr  13758  leexp2r  13890  hashbclem  14162  wrd2ind  14434  rtrclreclem3  14769  rtrclreclem4  14770  relexpindlem  14772  rtrclind  14774  rlimresb  15272  summo  15427  fsum2dlem  15480  prodmo  15644  fprod2dlem  15688  bezoutlem3  16247  bezoutlem4  16248  ncoprmgcdne1b  16353  qredeu  16361  coprmproddvdslem  16365  prmdvdsncoprmbd  16429  pcqmul  16552  pcadd  16588  pockthg  16605  prmreclem2  16616  vdwlem10  16689  ramub1lem2  16726  prmgaplem6  16755  prmgaplem7  16756  cshwsdisj  16798  mreexexlem4d  17354  mreexdomd  17356  issubc3  17562  cofucl  17601  setcmon  17800  setcepi  17801  drsdirfi  18021  poslubmo  18127  posglbmo  18128  grpridd  18357  issubmd  18443  mndind  18464  ghmpreima  18854  gaorber  18912  psgnunilem4  19103  psgneu  19112  odcau  19207  pgpssslw  19217  fislw  19228  lsmsubm  19256  efgsfo  19343  gsum2d2  19573  pgpfac1lem5  19680  pgpfac1  19681  pgpfaclem2  19683  pgpfaclem3  19684  unitgrp  19907  lmodprop2d  20183  lsspropd  20277  lbsextlem4  20421  assapropd  21074  evlslem1  21290  mdetunilem8  21766  mdetuni0  21768  mdetmul  21770  neiint  22253  restbas  22307  iscnp4  22412  cnpco  22416  nrmsep  22506  regsep2  22525  ordthauslem  22532  1stcfb  22594  1stcrest  22602  2ndcctbss  22604  2ndcdisj  22605  2ndcomap  22607  dis2ndc  22609  nlly2i  22625  islly2  22633  hausllycmp  22643  lly1stc  22645  comppfsc  22681  ptbasin  22726  txcls  22753  ptcnp  22771  txlly  22785  txnlly  22786  txtube  22789  txcmplem1  22790  txcmplem2  22791  xkococnlem  22808  basqtop  22860  regr1lem  22888  kqreglem1  22890  kqreglem2  22891  kqnrmlem1  22892  kqnrmlem2  22893  reghmph  22942  nrmhmph  22943  opnfbas  22991  rnelfmlem  23101  fmufil  23108  fclscf  23174  fclsfnflim  23176  flimfnfcls  23177  uffclsflim  23180  cnpfcfi  23189  cnpfcf  23190  alexsubALTlem2  23197  alexsubALTlem4  23199  tgpconncompeqg  23261  ghmcnp  23264  qustgplem  23270  tsmsxp  23304  blssps  23575  blss  23576  blcld  23659  metequiv2  23664  met2ndci  23676  prdsxmslem2  23683  txmetcnp  23701  nlmvscnlem1  23848  xrge0tsms  23995  ipcnlem1  24407  iscmet3  24455  metsscmetcld  24477  minveclem3  24591  pmltpc  24612  ovolscalem2  24676  ovolicc2lem5  24683  ovolicc2  24684  nulmbl2  24698  ioombl1  24724  uniioombllem6  24750  uniioombl  24751  vitalilem3  24772  i1faddlem  24855  mbfmullem  24888  itg2split  24912  lhop2  25177  dvfsumrlim  25193  itgsubst  25211  plydivex  25455  plyexmo  25471  ulmbdd  25555  cxploglim  26125  dchrptlem2  26411  lgsquad2lem2  26531  2sqlem5  26568  dchrvmasumif  26649  rpvmasum2  26658  dchrisum0re  26659  dchrisum0lem3  26665  dchrisum0  26666  dchrmusum  26670  dchrvmasum  26671  pntibndlem3  26738  pntlemp  26756  ostth3  26784  legtrid  26950  hlcgreu  26977  mirreu3  27013  midexlem  27051  opphllem  27094  mideulem  27095  opphllem1  27106  oppperpex  27112  lnperpex  27162  trgcopy  27163  iscgra1  27169  cgraswap  27179  cgracom  27181  cgratr  27182  flatcgra  27183  acopyeu  27193  ax5seglem9  27303  ax5seg  27304  axcontlem8  27337  axcontlem12  27341  clwwlknonwwlknonb  28466  2pthfrgr  28644  frgrnbnb  28653  ablo4  28908  smcnlem  29055  pjhthmo  29660  mdslmd1lem1  30683  xrge0tsmsd  31313  locfinref  31787  xpinpreima2  31853  qqhval2  31928  dya2iocnrect  32244  orvcgteel  32430  orvclteel  32435  derangenlem  33129  cnpconn  33188  txpconn  33190  connpconn  33193  pconnpi1  33195  iccllysconn  33208  rellysconn  33209  cvmcov2  33233  cvmliftmolem2  33240  cvmliftmo  33242  cvmliftlem15  33256  cvmliftpht  33276  cvmlift3lem2  33278  naddssim  33833  nosupbday  33904  nosupbnd1lem1  33907  nosupbnd2  33915  noinfno  33917  noinfbday  33919  noinfbnd1lem1  33922  noinfbnd2  33930  conway  33989  madebdaylemlrcut  34075  cgrextend  34306  btwnouttr2  34320  cgrsub  34343  cgrxfr  34353  btwnxfr  34354  colineardim1  34359  btwnconn1lem6  34390  btwnconn1lem13  34397  btwnconn1lem14  34398  btwnconn3  34401  seglecgr12im  34408  segleantisym  34413  outsideofeq  34428  outsidele  34430  lineunray  34445  linethru  34451  fnessref  34542  neibastop2lem  34545  neibastop2  34546  unblimceq0lem  34682  knoppndvlem22  34709  bj-finsumval0  35452  isbasisrelowllem1  35522  isbasisrelowllem2  35523  mblfinlem3  35812  cnambfre  35821  areacirclem5  35865  istotbnd3  35925  sstotbnd  35929  crngm4  36157  cvlcvr1  37349  4atlem12  37622  paddasslem10  37839  paddasslem12  37841  paddasslem13  37842  lhpexle3lem  38021  cdlemd4  38211  cdleme0cq  38225  cdlemefs32sn1aw  38424  cdleme43fsv1snlem  38430  cdleme32d  38454  cdleme32f  38456  cdleme40m  38477  cdleme40n  38478  cdleme42keg  38496  cdleme42mgN  38498  cdleme50trn2  38561  cdleme50trn3  38563  cdlemm10N  39128  dihvalcqpre  39245  dihopelvalcpre  39258  dihmeetlem1N  39300  dihjat1lem  39438  mapd0  39675  mapdh9a  39799  fsuppssind  40279  nna4b4nsq  40494  diophin  40591  pellexlem3  40650  pellexlem5  40652  pellex  40654  pell14qrmulcl  40682  jm2.19lem3  40810  jm2.25  40818  jm2.27b  40825  lmhmfgsplit  40908  hbtlem2  40946  hbtlem5  40950  gsumws3  41777  gsumws4  41778  mnuprdlem4  41863  fnchoice  42542  stoweidlem17  43529  stoweidlem53  43565  stoweidlem61  43573  qndenserrnbllem  43806  bgoldbtbnd  45230  rabsubmgmd  45314  lindslinindsimp1  45767  prsthinc  46304