Theorem simprrl 779

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  prproe  4838  f1prex  7042  wfrlem17  7973  eroveu  8394  undom  8607  mapdom2  8690  domunfican  8793  fofinf1o  8801  finsschain  8833  wemaplem3  9014  oemapvali  9149  iunfictbso  9542  enfin2i  9745  fin1a2s  9838  ttukeylem6  9938  distrlem4pr  10450  mulcmpblnr  10495  prsrlem1  10496  dedekind  10805  divdivdiv  11343  divmuleq  11347  divsubdiv  11358  lediv12a  11535  xralrple  12601  ssfzo12bi  13135  seqcaopr  13410  leexp2r  13541  hashbclem  13813  wrd2ind  14087  rtrclreclem3  14421  rtrclreclem4  14422  relexpindlem  14424  rtrclind  14426  rlimresb  14924  summo  15076  fsum2dlem  15127  prodmo  15292  fprod2dlem  15336  bezoutlem3  15891  bezoutlem4  15892  ncoprmgcdne1b  15996  qredeu  16004  coprmproddvdslem  16008  pcqmul  16192  pcadd  16227  pockthg  16244  prmreclem2  16255  vdwlem10  16328  ramub1lem2  16365  prmgaplem6  16394  prmgaplem7  16395  cshwsdisj  16434  mreexexlem4d  16920  mreexdomd  16922  issubc3  17121  cofucl  17160  setcmon  17349  setcepi  17350  drsdirfi  17550  poslubmo  17758  posglbmo  17759  grpridd  17887  issubmd  17973  mndind  17994  ghmpreima  18382  gaorber  18440  psgnunilem4  18627  psgneu  18636  odcau  18731  pgpssslw  18741  fislw  18752  lsmsubm  18780  efgsfo  18867  gsum2d2  19096  pgpfac1lem5  19203  pgpfac1  19204  pgpfaclem2  19206  pgpfaclem3  19207  unitgrp  19419  lmodprop2d  19698  lsspropd  19791  lbsextlem4  19935  assapropd  20103  evlslem1  20297  mdetunilem8  21230  mdetuni0  21232  mdetmul  21234  neiint  21714  restbas  21768  iscnp4  21873  cnpco  21877  nrmsep  21967  regsep2  21986  ordthauslem  21993  1stcfb  22055  1stcrest  22063  2ndcctbss  22065  2ndcdisj  22066  2ndcomap  22068  dis2ndc  22070  nlly2i  22086  islly2  22094  hausllycmp  22104  lly1stc  22106  comppfsc  22142  ptbasin  22187  txcls  22214  ptcnp  22232  txlly  22246  txnlly  22247  txtube  22250  txcmplem1  22251  txcmplem2  22252  xkococnlem  22269  basqtop  22321  regr1lem  22349  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  reghmph  22403  nrmhmph  22404  opnfbas  22452  rnelfmlem  22562  fmufil  22569  fclscf  22635  fclsfnflim  22637  flimfnfcls  22638  uffclsflim  22641  cnpfcfi  22650  cnpfcf  22651  alexsubALTlem2  22658  alexsubALTlem4  22660  tgpconncompeqg  22722  ghmcnp  22725  qustgplem  22731  tsmsxp  22765  blssps  23036  blss  23037  blcld  23117  metequiv2  23122  met2ndci  23134  prdsxmslem2  23141  txmetcnp  23159  nlmvscnlem1  23297  xrge0tsms  23444  ipcnlem1  23850  iscmet3  23898  metsscmetcld  23920  minveclem3  24034  pmltpc  24053  ovolscalem2  24117  ovolicc2lem5  24124  ovolicc2  24125  nulmbl2  24139  ioombl1  24165  uniioombllem6  24191  uniioombl  24192  vitalilem3  24213  i1faddlem  24296  mbfmullem  24328  itg2split  24352  lhop2  24614  dvfsumrlim  24630  itgsubst  24648  plydivex  24888  plyexmo  24904  ulmbdd  24988  cxploglim  25557  dchrptlem2  25843  lgsquad2lem2  25963  2sqlem5  26000  dchrvmasumif  26081  rpvmasum2  26090  dchrisum0re  26091  dchrisum0lem3  26097  dchrisum0  26098  dchrmusum  26102  dchrvmasum  26103  pntibndlem3  26170  pntlemp  26188  ostth3  26216  legtrid  26379  hlcgreu  26406  mirreu3  26442  midexlem  26480  opphllem  26523  mideulem  26524  opphllem1  26535  oppperpex  26541  lnperpex  26591  trgcopy  26592  iscgra1  26598  cgraswap  26608  cgracom  26610  cgratr  26611  flatcgra  26612  acopyeu  26622  ax5seglem9  26725  ax5seg  26726  axcontlem8  26759  axcontlem12  26763  clwwlknonwwlknonb  27887  2pthfrgr  28065  frgrnbnb  28074  ablo4  28329  smcnlem  28476  pjhthmo  29081  mdslmd1lem1  30104  xrge0tsmsd  30694  locfinref  31107  xpinpreima2  31152  qqhval2  31225  dya2iocnrect  31541  orvcgteel  31727  orvclteel  31732  derangenlem  32420  cnpconn  32479  txpconn  32481  connpconn  32484  pconnpi1  32486  iccllysconn  32499  rellysconn  32500  cvmcov2  32524  cvmliftmolem2  32531  cvmliftmo  32533  cvmliftlem15  32547  cvmliftpht  32567  cvmlift3lem2  32569  fpr3g  33124  nosupbnd1lem1  33210  nosupbnd2  33218  conway  33266  cgrextend  33471  btwnouttr2  33485  cgrsub  33508  cgrxfr  33518  btwnxfr  33519  colineardim1  33524  btwnconn1lem6  33555  btwnconn1lem13  33562  btwnconn1lem14  33563  btwnconn3  33566  seglecgr12im  33573  segleantisym  33578  outsideofeq  33593  outsidele  33595  lineunray  33610  linethru  33616  fnessref  33707  neibastop2lem  33710  neibastop2  33711  unblimceq0lem  33847  knoppndvlem22  33874  bj-finsumval0  34569  isbasisrelowllem1  34638  isbasisrelowllem2  34639  mblfinlem3  34933  cnambfre  34942  areacirclem5  34988  istotbnd3  35051  sstotbnd  35055  crngm4  35283  cvlcvr1  36477  4atlem12  36750  paddasslem10  36967  paddasslem12  36969  paddasslem13  36970  lhpexle3lem  37149  cdlemd4  37339  cdleme0cq  37353  cdlemefs32sn1aw  37552  cdleme43fsv1snlem  37558  cdleme32d  37582  cdleme32f  37584  cdleme40m  37605  cdleme40n  37606  cdleme42keg  37624  cdleme42mgN  37626  cdleme50trn2  37689  cdleme50trn3  37691  cdlemm10N  38256  dihvalcqpre  38373  dihopelvalcpre  38386  dihmeetlem1N  38428  dihjat1lem  38566  mapd0  38803  mapdh9a  38927  diophin  39376  pellexlem3  39435  pellexlem5  39437  pellex  39439  pell14qrmulcl  39467  jm2.19lem3  39595  jm2.25  39603  jm2.27b  39610  lmhmfgsplit  39693  hbtlem2  39731  hbtlem5  39735  gsumws3  40556  gsumws4  40557  mnuprdlem4  40618  fnchoice  41293  stoweidlem17  42309  stoweidlem53  42345  stoweidlem61  42353  qndenserrnbllem  42586  bgoldbtbnd  43981  rabsubmgmd  44065  lindslinindsimp1  44519