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  4857  f1prex  7218  fpr3g  8215  fprresex  8240  nnaordex2  8554  naddssim  8600  eroveu  8736  mapdom2  9061  domunfican  9206  fofinf1o  9216  finsschain  9243  wemaplem3  9434  oemapvali  9574  iunfictbso  10002  enfin2i  10209  fin1a2s  10302  ttukeylem6  10402  distrlem4pr  10914  mulcmpblnr  10959  prsrlem1  10960  dedekind  11273  divdivdiv  11819  divmuleq  11823  divsubdiv  11834  lediv12a  12012  xralrple  13101  ssfzo12bi  13658  seqcaopr  13943  leexp2r  14078  hashbclem  14356  wrd2ind  14627  rtrclreclem3  14964  rtrclreclem4  14965  relexpindlem  14967  rtrclind  14969  rlimresb  15469  summo  15621  fsum2dlem  15674  prodmo  15840  fprod2dlem  15884  bezoutlem3  16449  bezoutlem4  16450  ncoprmgcdne1b  16558  qredeu  16566  coprmproddvdslem  16570  prmdvdsncoprmbd  16635  pcqmul  16762  pcadd  16798  pockthg  16815  prmreclem2  16826  vdwlem10  16899  ramub1lem2  16936  prmgaplem6  16965  prmgaplem7  16966  cshwsdisj  17007  mreexexlem4d  17550  mreexdomd  17552  issubc3  17753  cofucl  17792  setcmon  17991  setcepi  17992  drsdirfi  18208  poslubmo  18312  posglbmo  18313  grprida  18580  rabsubmgmd  18609  issubmd  18711  mndind  18733  ghmpreima  19148  gaorber  19218  psgnunilem4  19407  psgneu  19416  odcau  19514  pgpssslw  19524  fislw  19535  lsmsubm  19563  efgsfo  19649  gsum2d2  19884  pgpfac1lem5  19991  pgpfac1  19992  pgpfaclem2  19994  pgpfaclem3  19995  unitgrp  20299  lmodprop2d  20855  lsspropd  20949  lbsextlem4  21096  assapropd  21807  evlslem1  22015  mdetunilem8  22532  mdetuni0  22534  mdetmul  22536  neiint  23017  restbas  23071  iscnp4  23176  cnpco  23180  nrmsep  23270  regsep2  23289  ordthauslem  23296  1stcfb  23358  1stcrest  23366  2ndcctbss  23368  2ndcdisj  23369  2ndcomap  23371  dis2ndc  23373  nlly2i  23389  islly2  23397  hausllycmp  23407  lly1stc  23409  comppfsc  23445  ptbasin  23490  txcls  23517  ptcnp  23535  txlly  23549  txnlly  23550  txtube  23553  txcmplem1  23554  txcmplem2  23555  xkococnlem  23572  basqtop  23624  regr1lem  23652  kqreglem1  23654  kqreglem2  23655  kqnrmlem1  23656  kqnrmlem2  23657  reghmph  23706  nrmhmph  23707  opnfbas  23755  rnelfmlem  23865  fmufil  23872  fclscf  23938  fclsfnflim  23940  flimfnfcls  23941  uffclsflim  23944  cnpfcfi  23953  cnpfcf  23954  alexsubALTlem2  23961  alexsubALTlem4  23963  tgpconncompeqg  24025  ghmcnp  24028  qustgplem  24034  tsmsxp  24068  blssps  24337  blss  24338  blcld  24418  metequiv2  24423  met2ndci  24435  prdsxmslem2  24442  txmetcnp  24460  nlmvscnlem1  24599  xrge0tsms  24748  ipcnlem1  25170  iscmet3  25218  metsscmetcld  25240  minveclem3  25354  pmltpc  25376  ovolscalem2  25440  ovolicc2lem5  25447  ovolicc2  25448  nulmbl2  25462  ioombl1  25488  uniioombllem6  25514  uniioombl  25515  vitalilem3  25536  i1faddlem  25619  mbfmullem  25651  itg2split  25675  lhop2  25945  dvfsumrlim  25963  itgsubst  25981  plydivex  26230  plyexmo  26246  ulmbdd  26332  cxploglim  26913  dchrptlem2  27201  lgsquad2lem2  27321  2sqlem5  27358  dchrvmasumif  27439  rpvmasum2  27448  dchrisum0re  27449  dchrisum0lem3  27455  dchrisum0  27456  dchrmusum  27460  dchrvmasum  27461  pntibndlem3  27528  pntlemp  27546  ostth3  27574  nosupbday  27642  nosupbnd1lem1  27645  nosupbnd2  27653  noinfno  27655  noinfbday  27657  noinfbnd1lem1  27660  noinfbnd2  27668  conway  27738  madebdaylemlrcut  27842  mulsproplem9  28061  mulsproplem13  28065  mulsproplem14  28066  mulsuniflem  28086  uzsind  28327  readdscl  28399  legtrid  28567  hlcgreu  28594  mirreu3  28630  midexlem  28668  opphllem  28711  mideulem  28712  opphllem1  28723  oppperpex  28729  lnperpex  28779  trgcopy  28780  iscgra1  28786  cgraswap  28796  cgracom  28798  cgratr  28799  flatcgra  28800  acopyeu  28810  ax5seglem9  28913  ax5seg  28914  axcontlem8  28947  axcontlem12  28951  clwwlknonwwlknonb  30081  2pthfrgr  30259  frgrnbnb  30268  ablo4  30525  smcnlem  30672  pjhthmo  31277  mdslmd1lem1  32300  xrge0tsmsd  33037  locfinref  33849  xpinpreima2  33915  qqhval2  33990  dya2iocnrect  34289  orvcgteel  34476  orvclteel  34481  derangenlem  35203  cnpconn  35262  txpconn  35264  connpconn  35267  pconnpi1  35269  iccllysconn  35282  rellysconn  35283  cvmcov2  35307  cvmliftmolem2  35314  cvmliftmo  35316  cvmliftlem15  35330  cvmliftpht  35350  cvmlift3lem2  35352  cgrextend  36041  btwnouttr2  36055  cgrsub  36078  cgrxfr  36088  btwnxfr  36089  colineardim1  36094  btwnconn1lem6  36125  btwnconn1lem13  36132  btwnconn1lem14  36133  btwnconn3  36136  seglecgr12im  36143  segleantisym  36148  outsideofeq  36163  outsidele  36165  lineunray  36180  linethru  36186  fnessref  36390  neibastop2lem  36393  neibastop2  36394  weiunpo  36498  unblimceq0lem  36539  knoppndvlem22  36566  bj-finsumval0  37318  isbasisrelowllem1  37388  isbasisrelowllem2  37389  mblfinlem3  37698  cnambfre  37707  areacirclem5  37751  istotbnd3  37810  sstotbnd  37814  crngm4  38042  cvlcvr1  39377  4atlem12  39650  paddasslem10  39867  paddasslem12  39869  paddasslem13  39870  lhpexle3lem  40049  cdlemd4  40239  cdleme0cq  40253  cdlemefs32sn1aw  40452  cdleme43fsv1snlem  40458  cdleme32d  40482  cdleme32f  40484  cdleme40m  40505  cdleme40n  40506  cdleme42keg  40524  cdleme42mgN  40526  cdleme50trn2  40589  cdleme50trn3  40591  cdlemm10N  41156  dihvalcqpre  41273  dihopelvalcpre  41286  dihmeetlem1N  41328  dihjat1lem  41466  mapd0  41703  mapdh9a  41827  fsuppssind  42625  nna4b4nsq  42692  diophin  42804  pellexlem3  42863  pellexlem5  42865  pellex  42867  pell14qrmulcl  42895  jm2.19lem3  43023  jm2.25  43031  jm2.27b  43038  lmhmfgsplit  43118  hbtlem2  43156  hbtlem5  43160  gsumws3  44228  gsumws4  44229  mnuprdlem4  44307  fnchoice  45065  stoweidlem17  46054  stoweidlem53  46090  stoweidlem61  46098  qndenserrnbllem  46331  bgoldbtbnd  47839  cycldlenngric  47958  isubgr3stgrlem6  48001  lindslinindsimp1  48488  brab2dd  48858  prsthinc  49495