Theorem simprrl 780

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4859  f1prex  7225  fpr3g  8225  fprresex  8250  nnaordex2  8564  naddssim  8610  eroveu  8746  mapdom2  9072  domunfican  9230  fofinf1o  9241  finsschain  9268  wemaplem3  9459  oemapvali  9599  iunfictbso  10027  enfin2i  10234  fin1a2s  10327  ttukeylem6  10427  distrlem4pr  10939  mulcmpblnr  10984  prsrlem1  10985  dedekind  11297  divdivdiv  11843  divmuleq  11847  divsubdiv  11858  lediv12a  12036  xralrple  13125  ssfzo12bi  13682  seqcaopr  13964  leexp2r  14099  hashbclem  14377  wrd2ind  14647  rtrclreclem3  14985  rtrclreclem4  14986  relexpindlem  14988  rtrclind  14990  rlimresb  15490  summo  15642  fsum2dlem  15695  prodmo  15861  fprod2dlem  15905  bezoutlem3  16470  bezoutlem4  16471  ncoprmgcdne1b  16579  qredeu  16587  coprmproddvdslem  16591  prmdvdsncoprmbd  16656  pcqmul  16783  pcadd  16819  pockthg  16836  prmreclem2  16847  vdwlem10  16920  ramub1lem2  16957  prmgaplem6  16986  prmgaplem7  16987  cshwsdisj  17028  mreexexlem4d  17571  mreexdomd  17573  issubc3  17774  cofucl  17813  setcmon  18012  setcepi  18013  drsdirfi  18229  poslubmo  18333  posglbmo  18334  grprida  18567  rabsubmgmd  18596  issubmd  18698  mndind  18720  ghmpreima  19135  gaorber  19205  psgnunilem4  19394  psgneu  19403  odcau  19501  pgpssslw  19511  fislw  19522  lsmsubm  19550  efgsfo  19636  gsum2d2  19871  pgpfac1lem5  19978  pgpfac1  19979  pgpfaclem2  19981  pgpfaclem3  19982  unitgrp  20286  lmodprop2d  20845  lsspropd  20939  lbsextlem4  21086  assapropd  21797  evlslem1  22005  mdetunilem8  22522  mdetuni0  22524  mdetmul  22526  neiint  23007  restbas  23061  iscnp4  23166  cnpco  23170  nrmsep  23260  regsep2  23279  ordthauslem  23286  1stcfb  23348  1stcrest  23356  2ndcctbss  23358  2ndcdisj  23359  2ndcomap  23361  dis2ndc  23363  nlly2i  23379  islly2  23387  hausllycmp  23397  lly1stc  23399  comppfsc  23435  ptbasin  23480  txcls  23507  ptcnp  23525  txlly  23539  txnlly  23540  txtube  23543  txcmplem1  23544  txcmplem2  23545  xkococnlem  23562  basqtop  23614  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  reghmph  23696  nrmhmph  23697  opnfbas  23745  rnelfmlem  23855  fmufil  23862  fclscf  23928  fclsfnflim  23930  flimfnfcls  23931  uffclsflim  23934  cnpfcfi  23943  cnpfcf  23944  alexsubALTlem2  23951  alexsubALTlem4  23953  tgpconncompeqg  24015  ghmcnp  24018  qustgplem  24024  tsmsxp  24058  blssps  24328  blss  24329  blcld  24409  metequiv2  24414  met2ndci  24426  prdsxmslem2  24433  txmetcnp  24451  nlmvscnlem1  24590  xrge0tsms  24739  ipcnlem1  25161  iscmet3  25209  metsscmetcld  25231  minveclem3  25345  pmltpc  25367  ovolscalem2  25431  ovolicc2lem5  25438  ovolicc2  25439  nulmbl2  25453  ioombl1  25479  uniioombllem6  25505  uniioombl  25506  vitalilem3  25527  i1faddlem  25610  mbfmullem  25642  itg2split  25666  lhop2  25936  dvfsumrlim  25954  itgsubst  25972  plydivex  26221  plyexmo  26237  ulmbdd  26323  cxploglim  26904  dchrptlem2  27192  lgsquad2lem2  27312  2sqlem5  27349  dchrvmasumif  27430  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  dchrmusum  27451  dchrvmasum  27452  pntibndlem3  27519  pntlemp  27537  ostth3  27565  nosupbday  27633  nosupbnd1lem1  27636  nosupbnd2  27644  noinfno  27646  noinfbday  27648  noinfbnd1lem1  27651  noinfbnd2  27659  conway  27728  madebdaylemlrcut  27831  mulsproplem9  28050  mulsproplem13  28054  mulsproplem14  28055  mulsuniflem  28075  uzsind  28316  readdscl  28386  legtrid  28554  hlcgreu  28581  mirreu3  28617  midexlem  28655  opphllem  28698  mideulem  28699  opphllem1  28710  oppperpex  28716  lnperpex  28766  trgcopy  28767  iscgra1  28773  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  acopyeu  28797  ax5seglem9  28900  ax5seg  28901  axcontlem8  28934  axcontlem12  28938  clwwlknonwwlknonb  30068  2pthfrgr  30246  frgrnbnb  30255  ablo4  30512  smcnlem  30659  pjhthmo  31264  mdslmd1lem1  32287  xrge0tsmsd  33028  locfinref  33807  xpinpreima2  33873  qqhval2  33948  dya2iocnrect  34248  orvcgteel  34435  orvclteel  34440  derangenlem  35143  cnpconn  35202  txpconn  35204  connpconn  35207  pconnpi1  35209  iccllysconn  35222  rellysconn  35223  cvmcov2  35247  cvmliftmolem2  35254  cvmliftmo  35256  cvmliftlem15  35270  cvmliftpht  35290  cvmlift3lem2  35292  cgrextend  35981  btwnouttr2  35995  cgrsub  36018  cgrxfr  36028  btwnxfr  36029  colineardim1  36034  btwnconn1lem6  36065  btwnconn1lem13  36072  btwnconn1lem14  36073  btwnconn3  36076  seglecgr12im  36083  segleantisym  36088  outsideofeq  36103  outsidele  36105  lineunray  36120  linethru  36126  fnessref  36330  neibastop2lem  36333  neibastop2  36334  weiunpo  36438  unblimceq0lem  36479  knoppndvlem22  36506  bj-finsumval0  37258  isbasisrelowllem1  37328  isbasisrelowllem2  37329  mblfinlem3  37638  cnambfre  37647  areacirclem5  37691  istotbnd3  37750  sstotbnd  37754  crngm4  37982  cvlcvr1  39317  4atlem12  39591  paddasslem10  39808  paddasslem12  39810  paddasslem13  39811  lhpexle3lem  39990  cdlemd4  40180  cdleme0cq  40194  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme32d  40423  cdleme32f  40425  cdleme40m  40446  cdleme40n  40447  cdleme42keg  40465  cdleme42mgN  40467  cdleme50trn2  40530  cdleme50trn3  40532  cdlemm10N  41097  dihvalcqpre  41214  dihopelvalcpre  41227  dihmeetlem1N  41269  dihjat1lem  41407  mapd0  41644  mapdh9a  41768  fsuppssind  42566  nna4b4nsq  42633  diophin  42745  pellexlem3  42804  pellexlem5  42806  pellex  42808  pell14qrmulcl  42836  jm2.19lem3  42964  jm2.25  42972  jm2.27b  42979  lmhmfgsplit  43059  hbtlem2  43097  hbtlem5  43101  gsumws3  44169  gsumws4  44170  mnuprdlem4  44248  fnchoice  45007  stoweidlem17  45999  stoweidlem53  46035  stoweidlem61  46043  qndenserrnbllem  46276  bgoldbtbnd  47794  cycldlenngric  47913  isubgr3stgrlem6  47956  lindslinindsimp1  48443  brab2dd  48813  prsthinc  49450