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 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  4905  f1prex  7304  fpr3g  8310  fprresex  8335  wfrlem17OLD  8365  nnaordex2  8677  naddssim  8723  eroveu  8852  undomOLD  9100  mapdom2  9188  domunfican  9361  fofinf1o  9372  finsschain  9399  wemaplem3  9588  oemapvali  9724  iunfictbso  10154  enfin2i  10361  fin1a2s  10454  ttukeylem6  10554  distrlem4pr  11066  mulcmpblnr  11111  prsrlem1  11112  dedekind  11424  divdivdiv  11968  divmuleq  11972  divsubdiv  11983  lediv12a  12161  xralrple  13247  ssfzo12bi  13800  seqcaopr  14080  leexp2r  14214  hashbclem  14491  wrd2ind  14761  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  rlimresb  15601  summo  15753  fsum2dlem  15806  prodmo  15972  fprod2dlem  16016  bezoutlem3  16578  bezoutlem4  16579  ncoprmgcdne1b  16687  qredeu  16695  coprmproddvdslem  16699  prmdvdsncoprmbd  16764  pcqmul  16891  pcadd  16927  pockthg  16944  prmreclem2  16955  vdwlem10  17028  ramub1lem2  17065  prmgaplem6  17094  prmgaplem7  17095  cshwsdisj  17136  mreexexlem4d  17690  mreexdomd  17692  issubc3  17894  cofucl  17933  setcmon  18132  setcepi  18133  drsdirfi  18351  poslubmo  18456  posglbmo  18457  grprida  18688  rabsubmgmd  18717  issubmd  18819  mndind  18841  ghmpreima  19256  gaorber  19326  psgnunilem4  19515  psgneu  19524  odcau  19622  pgpssslw  19632  fislw  19643  lsmsubm  19671  efgsfo  19757  gsum2d2  19992  pgpfac1lem5  20099  pgpfac1  20100  pgpfaclem2  20102  pgpfaclem3  20103  unitgrp  20383  lmodprop2d  20922  lsspropd  21016  lbsextlem4  21163  assapropd  21892  evlslem1  22106  mdetunilem8  22625  mdetuni0  22627  mdetmul  22629  neiint  23112  restbas  23166  iscnp4  23271  cnpco  23275  nrmsep  23365  regsep2  23384  ordthauslem  23391  1stcfb  23453  1stcrest  23461  2ndcctbss  23463  2ndcdisj  23464  2ndcomap  23466  dis2ndc  23468  nlly2i  23484  islly2  23492  hausllycmp  23502  lly1stc  23504  comppfsc  23540  ptbasin  23585  txcls  23612  ptcnp  23630  txlly  23644  txnlly  23645  txtube  23648  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  basqtop  23719  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  reghmph  23801  nrmhmph  23802  opnfbas  23850  rnelfmlem  23960  fmufil  23967  fclscf  24033  fclsfnflim  24035  flimfnfcls  24036  uffclsflim  24039  cnpfcfi  24048  cnpfcf  24049  alexsubALTlem2  24056  alexsubALTlem4  24058  tgpconncompeqg  24120  ghmcnp  24123  qustgplem  24129  tsmsxp  24163  blssps  24434  blss  24435  blcld  24518  metequiv2  24523  met2ndci  24535  prdsxmslem2  24542  txmetcnp  24560  nlmvscnlem1  24707  xrge0tsms  24856  ipcnlem1  25279  iscmet3  25327  metsscmetcld  25349  minveclem3  25463  pmltpc  25485  ovolscalem2  25549  ovolicc2lem5  25556  ovolicc2  25557  nulmbl2  25571  ioombl1  25597  uniioombllem6  25623  uniioombl  25624  vitalilem3  25645  i1faddlem  25728  mbfmullem  25760  itg2split  25784  lhop2  26054  dvfsumrlim  26072  itgsubst  26090  plydivex  26339  plyexmo  26355  ulmbdd  26441  cxploglim  27021  dchrptlem2  27309  lgsquad2lem2  27429  2sqlem5  27466  dchrvmasumif  27547  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  dchrmusum  27568  dchrvmasum  27569  pntibndlem3  27636  pntlemp  27654  ostth3  27682  nosupbday  27750  nosupbnd1lem1  27753  nosupbnd2  27761  noinfno  27763  noinfbday  27765  noinfbnd1lem1  27768  noinfbnd2  27776  conway  27844  madebdaylemlrcut  27937  mulsproplem9  28150  mulsproplem13  28154  mulsproplem14  28155  mulsuniflem  28175  uzsind  28391  readdscl  28431  legtrid  28599  hlcgreu  28626  mirreu3  28662  midexlem  28700  opphllem  28743  mideulem  28744  opphllem1  28755  oppperpex  28761  lnperpex  28811  trgcopy  28812  iscgra1  28818  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  acopyeu  28842  ax5seglem9  28952  ax5seg  28953  axcontlem8  28986  axcontlem12  28990  clwwlknonwwlknonb  30125  2pthfrgr  30303  frgrnbnb  30312  ablo4  30569  smcnlem  30716  pjhthmo  31321  mdslmd1lem1  32344  xrge0tsmsd  33065  locfinref  33840  xpinpreima2  33906  qqhval2  33983  dya2iocnrect  34283  orvcgteel  34470  orvclteel  34475  derangenlem  35176  cnpconn  35235  txpconn  35237  connpconn  35240  pconnpi1  35242  iccllysconn  35255  rellysconn  35256  cvmcov2  35280  cvmliftmolem2  35287  cvmliftmo  35289  cvmliftlem15  35303  cvmliftpht  35323  cvmlift3lem2  35325  cgrextend  36009  btwnouttr2  36023  cgrsub  36046  cgrxfr  36056  btwnxfr  36057  colineardim1  36062  btwnconn1lem6  36093  btwnconn1lem13  36100  btwnconn1lem14  36101  btwnconn3  36104  seglecgr12im  36111  segleantisym  36116  outsideofeq  36131  outsidele  36133  lineunray  36148  linethru  36154  fnessref  36358  neibastop2lem  36361  neibastop2  36362  weiunpo  36466  unblimceq0lem  36507  knoppndvlem22  36534  bj-finsumval0  37286  isbasisrelowllem1  37356  isbasisrelowllem2  37357  mblfinlem3  37666  cnambfre  37675  areacirclem5  37719  istotbnd3  37778  sstotbnd  37782  crngm4  38010  cvlcvr1  39340  4atlem12  39614  paddasslem10  39831  paddasslem12  39833  paddasslem13  39834  lhpexle3lem  40013  cdlemd4  40203  cdleme0cq  40217  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  cdleme42keg  40488  cdleme42mgN  40490  cdleme50trn2  40553  cdleme50trn3  40555  cdlemm10N  41120  dihvalcqpre  41237  dihopelvalcpre  41250  dihmeetlem1N  41292  dihjat1lem  41430  mapd0  41667  mapdh9a  41791  fsuppssind  42603  nna4b4nsq  42670  diophin  42783  pellexlem3  42842  pellexlem5  42844  pellex  42846  pell14qrmulcl  42874  jm2.19lem3  43003  jm2.25  43011  jm2.27b  43018  lmhmfgsplit  43098  hbtlem2  43136  hbtlem5  43140  gsumws3  44209  gsumws4  44210  mnuprdlem4  44294  fnchoice  45034  stoweidlem17  46032  stoweidlem53  46068  stoweidlem61  46076  qndenserrnbllem  46309  bgoldbtbnd  47796  isubgr3stgrlem6  47938  lindslinindsimp1  48374  brab2dd  48741  prsthinc  49111