Theorem simprrl 781

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 729	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 210  df-an 400

This theorem is referenced by:  prproe  4803  f1prex  7072  fpr3g  8004  wfrlem17  8049  eroveu  8472  undom  8711  mapdom2  8795  domunfican  8922  fofinf1o  8929  finsschain  8961  wemaplem3  9142  oemapvali  9277  iunfictbso  9693  enfin2i  9900  fin1a2s  9993  ttukeylem6  10093  distrlem4pr  10605  mulcmpblnr  10650  prsrlem1  10651  dedekind  10960  divdivdiv  11498  divmuleq  11502  divsubdiv  11513  lediv12a  11690  xralrple  12760  ssfzo12bi  13302  seqcaopr  13578  leexp2r  13709  hashbclem  13981  wrd2ind  14253  rtrclreclem3  14588  rtrclreclem4  14589  relexpindlem  14591  rtrclind  14593  rlimresb  15091  summo  15246  fsum2dlem  15297  prodmo  15461  fprod2dlem  15505  bezoutlem3  16064  bezoutlem4  16065  ncoprmgcdne1b  16170  qredeu  16178  coprmproddvdslem  16182  prmdvdsncoprmbd  16246  pcqmul  16369  pcadd  16405  pockthg  16422  prmreclem2  16433  vdwlem10  16506  ramub1lem2  16543  prmgaplem6  16572  prmgaplem7  16573  cshwsdisj  16615  mreexexlem4d  17104  mreexdomd  17106  issubc3  17309  cofucl  17348  setcmon  17547  setcepi  17548  drsdirfi  17766  poslubmo  17871  posglbmo  17872  grpridd  18101  issubmd  18187  mndind  18208  ghmpreima  18598  gaorber  18656  psgnunilem4  18843  psgneu  18852  odcau  18947  pgpssslw  18957  fislw  18968  lsmsubm  18996  efgsfo  19083  gsum2d2  19313  pgpfac1lem5  19420  pgpfac1  19421  pgpfaclem2  19423  pgpfaclem3  19424  unitgrp  19639  lmodprop2d  19915  lsspropd  20008  lbsextlem4  20152  assapropd  20785  evlslem1  20996  mdetunilem8  21470  mdetuni0  21472  mdetmul  21474  neiint  21955  restbas  22009  iscnp4  22114  cnpco  22118  nrmsep  22208  regsep2  22227  ordthauslem  22234  1stcfb  22296  1stcrest  22304  2ndcctbss  22306  2ndcdisj  22307  2ndcomap  22309  dis2ndc  22311  nlly2i  22327  islly2  22335  hausllycmp  22345  lly1stc  22347  comppfsc  22383  ptbasin  22428  txcls  22455  ptcnp  22473  txlly  22487  txnlly  22488  txtube  22491  txcmplem1  22492  txcmplem2  22493  xkococnlem  22510  basqtop  22562  regr1lem  22590  kqreglem1  22592  kqreglem2  22593  kqnrmlem1  22594  kqnrmlem2  22595  reghmph  22644  nrmhmph  22645  opnfbas  22693  rnelfmlem  22803  fmufil  22810  fclscf  22876  fclsfnflim  22878  flimfnfcls  22879  uffclsflim  22882  cnpfcfi  22891  cnpfcf  22892  alexsubALTlem2  22899  alexsubALTlem4  22901  tgpconncompeqg  22963  ghmcnp  22966  qustgplem  22972  tsmsxp  23006  blssps  23276  blss  23277  blcld  23357  metequiv2  23362  met2ndci  23374  prdsxmslem2  23381  txmetcnp  23399  nlmvscnlem1  23538  xrge0tsms  23685  ipcnlem1  24096  iscmet3  24144  metsscmetcld  24166  minveclem3  24280  pmltpc  24301  ovolscalem2  24365  ovolicc2lem5  24372  ovolicc2  24373  nulmbl2  24387  ioombl1  24413  uniioombllem6  24439  uniioombl  24440  vitalilem3  24461  i1faddlem  24544  mbfmullem  24577  itg2split  24601  lhop2  24866  dvfsumrlim  24882  itgsubst  24900  plydivex  25144  plyexmo  25160  ulmbdd  25244  cxploglim  25814  dchrptlem2  26100  lgsquad2lem2  26220  2sqlem5  26257  dchrvmasumif  26338  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lem3  26354  dchrisum0  26355  dchrmusum  26359  dchrvmasum  26360  pntibndlem3  26427  pntlemp  26445  ostth3  26473  legtrid  26636  hlcgreu  26663  mirreu3  26699  midexlem  26737  opphllem  26780  mideulem  26781  opphllem1  26792  oppperpex  26798  lnperpex  26848  trgcopy  26849  iscgra1  26855  cgraswap  26865  cgracom  26867  cgratr  26868  flatcgra  26869  acopyeu  26879  ax5seglem9  26982  ax5seg  26983  axcontlem8  27016  axcontlem12  27020  clwwlknonwwlknonb  28143  2pthfrgr  28321  frgrnbnb  28330  ablo4  28585  smcnlem  28732  pjhthmo  29337  mdslmd1lem1  30360  xrge0tsmsd  30990  locfinref  31459  xpinpreima2  31525  qqhval2  31598  dya2iocnrect  31914  orvcgteel  32100  orvclteel  32105  derangenlem  32800  cnpconn  32859  txpconn  32861  connpconn  32864  pconnpi1  32866  iccllysconn  32879  rellysconn  32880  cvmcov2  32904  cvmliftmolem2  32911  cvmliftmo  32913  cvmliftlem15  32927  cvmliftpht  32947  cvmlift3lem2  32949  naddssim  33523  nosupbday  33594  nosupbnd1lem1  33597  nosupbnd2  33605  noinfno  33607  noinfbday  33609  noinfbnd1lem1  33612  noinfbnd2  33620  conway  33679  madebdaylemlrcut  33765  cgrextend  33996  btwnouttr2  34010  cgrsub  34033  cgrxfr  34043  btwnxfr  34044  colineardim1  34049  btwnconn1lem6  34080  btwnconn1lem13  34087  btwnconn1lem14  34088  btwnconn3  34091  seglecgr12im  34098  segleantisym  34103  outsideofeq  34118  outsidele  34120  lineunray  34135  linethru  34141  fnessref  34232  neibastop2lem  34235  neibastop2  34236  unblimceq0lem  34372  knoppndvlem22  34399  bj-finsumval0  35140  isbasisrelowllem1  35212  isbasisrelowllem2  35213  mblfinlem3  35502  cnambfre  35511  areacirclem5  35555  istotbnd3  35615  sstotbnd  35619  crngm4  35847  cvlcvr1  37039  4atlem12  37312  paddasslem10  37529  paddasslem12  37531  paddasslem13  37532  lhpexle3lem  37711  cdlemd4  37901  cdleme0cq  37915  cdlemefs32sn1aw  38114  cdleme43fsv1snlem  38120  cdleme32d  38144  cdleme32f  38146  cdleme40m  38167  cdleme40n  38168  cdleme42keg  38186  cdleme42mgN  38188  cdleme50trn2  38251  cdleme50trn3  38253  cdlemm10N  38818  dihvalcqpre  38935  dihopelvalcpre  38948  dihmeetlem1N  38990  dihjat1lem  39128  mapd0  39365  mapdh9a  39489  fsuppssind  39933  nna4b4nsq  40141  diophin  40238  pellexlem3  40297  pellexlem5  40299  pellex  40301  pell14qrmulcl  40329  jm2.19lem3  40457  jm2.25  40465  jm2.27b  40472  lmhmfgsplit  40555  hbtlem2  40593  hbtlem5  40597  gsumws3  41426  gsumws4  41427  mnuprdlem4  41507  fnchoice  42186  stoweidlem17  43176  stoweidlem53  43212  stoweidlem61  43220  qndenserrnbllem  43453  bgoldbtbnd  44877  rabsubmgmd  44961  lindslinindsimp1  45414  prsthinc  45951