Theorem simprrr 782

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 730	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  4838  f1prex  7228  fliftfun  7256  fprresex  8249  nnaordex2  8564  naddssim  8610  mapdom2  9075  domunfican  9221  fofinf1o  9231  finsschain  9258  wemaplem3  9452  oemapvali  9594  iunfictbso  10025  enfin2i  10232  fin1a2s  10325  distrlem4pr  10938  mulcmpblnr  10983  prsrlem1  10984  addsrmo  10985  mulsrmo  10986  divdivdiv  11845  divsubdiv  11860  lediv12a  12038  xralrple  13146  seqcaopr  13990  leexp2r  14125  hashbclem  14403  wrd2ind  14674  cshwidxmod  14754  rtrclreclem4  15012  relexpindlem  15014  rtrclind  15016  rlimresb  15516  summo  15668  fsum2dlem  15721  prodmo  15890  fprod2dlem  15934  bezoutlem3  16499  bezoutlem4  16500  qredeu  16616  coprmproddvdslem  16620  prmdvdsncoprmbd  16686  pcqmul  16813  pcadd  16849  pockthg  16866  ramub1lem2  16987  cshwsdisj  17058  mreexexlem4d  17602  issubc3  17805  cofucl  17844  setcmon  18043  setcepi  18044  drsdirfi  18260  poslubmo  18364  posglbmo  18365  grprida  18632  ghmpreima  19202  gaorber  19272  psgnunilem4  19461  psgneu  19470  odcau  19568  pgpssslw  19578  fislw  19589  lsmsubm  19617  efgsfo  19703  pgpfac1  20046  pgpfaclem2  20048  pgpfaclem3  20049  unitgrp  20352  islmodd  20850  lmodprop2d  20908  lsspropd  21001  lbsextlem4  21148  assapropd  21840  evlslem1  22049  mdetunilem8  22572  mdetmul  22576  ppttop  22960  epttop  22962  restbas  23111  iscnp4  23216  cnpco  23220  nrmsep  23310  regsep2  23329  ordthauslem  23336  1stcfb  23398  2ndcctbss  23408  2ndcdisj  23409  2ndcomap  23411  dis2ndc  23413  1stcelcls  23414  nlly2i  23429  islly2  23437  hausllycmp  23447  lly1stc  23449  comppfsc  23485  1stckgenlem  23506  ptbasin  23530  txcls  23557  ptcnp  23575  txlly  23589  txnlly  23590  txtube  23593  txcmplem1  23594  txcmplem2  23595  xkococnlem  23612  basqtop  23664  regr1lem  23692  kqreglem1  23694  kqreglem2  23695  kqnrmlem1  23696  kqnrmlem2  23697  reghmph  23746  nrmhmph  23747  filuni  23838  rnelfmlem  23905  fmufil  23912  fclscf  23978  fclsfnflim  23980  flimfnfcls  23981  uffclsflim  23984  cnpfcfi  23993  cnpfcf  23994  alexsublem  23997  alexsubALTlem3  24002  tgpconncompeqg  24065  ghmcnp  24068  qustgplem  24074  blssps  24377  blss  24378  blcld  24458  metequiv2  24463  met2ndci  24475  prdsxmslem2  24482  txmetcnp  24500  nlmvscnlem1  24639  xrge0tsms  24788  ipcnlem1  25200  iscmet3  25248  metsscmetcld  25270  minveclem3  25384  pmltpc  25405  ovolscalem2  25469  ovolicc2lem5  25476  ovolicc2  25477  nulmbl2  25491  ioombl1  25517  uniioombllem6  25543  uniioombl  25544  vitalilem3  25565  i1faddlem  25648  mbfmullem  25680  itg2const2  25696  itg2split  25704  lhop2  25970  dvfsumrlim  25986  itgsubst  26004  plydivex  26251  plyexmo  26267  ulmbdd  26351  cxploglim  26929  dchrptlem2  27216  lgsquad2lem2  27336  2sqlem5  27373  dchrvmasumif  27454  rpvmasum2  27463  dchrisum0re  27464  dchrisum0lem3  27470  dchrisum0  27471  dchrmusum  27475  dchrvmasum  27476  pntibndlem3  27543  pntlemp  27561  ostth3  27589  nosupbday  27657  nosupbnd1lem1  27660  nosupbnd2  27668  noinfbday  27672  noinfbnd1lem1  27675  noinfbnd2  27683  conway  27759  madebdaylemlrcut  27879  mulsproplem9  28104  mulsuniflem  28129  uzsind  28385  bdayfinbndlem1  28447  readdscl  28479  legtrid  28647  hlcgreu  28674  mirreu3  28710  opphllem  28791  oppperpex  28809  lnperpex  28859  trgcopy  28860  iscgra1  28866  cgraswap  28876  cgracom  28878  cgratr  28879  flatcgra  28880  acopyeu  28890  ax5seglem9  28994  ax5seg  28995  axcontlem8  29028  axcontlem12  29032  upgrclwlkcompim  29837  wwlksnextwrd  29953  2pthfrgr  30342  frgrnbnb  30351  ablo4  30609  smcnlem  30756  pjhthmo  31361  1stpreimas  32767  xrge0tsmsd  33122  locfinref  33973  xpinpreima2  34039  qqhval2  34114  dya2iocnrect  34413  orvcgteel  34600  orvclteel  34605  cnpconn  35400  txpconn  35402  connpconn  35405  pconnpi1  35407  iccllysconn  35420  rellysconn  35421  cvmcov2  35445  cvmliftmolem2  35452  cvmliftmo  35454  cvmliftlem15  35468  cvmliftpht  35488  cvmlift3lem2  35490  cgrextend  36178  btwnouttr2  36192  btwnexch2  36193  cgrxfr  36225  lineext  36246  btwnconn1lem5  36261  btwnconn1lem13  36269  btwnconn3  36273  segletr  36284  segleantisym  36285  outsideofeq  36300  outsidele  36302  lineunray  36317  refssfne  36528  neibastop2lem  36530  neibastop2  36531  weiunpo  36635  unblimceq0lem  36754  knoppndvlem22  36781  mblfinlem3  37968  mblfinlem4  37969  cnambfre  37977  itg2addnclem  37980  areacirclem5  38021  istotbnd3  38080  crngm4  38312  cvlcvr1  39773  4atlem12  40046  cdlemb  40228  paddasslem10  40263  paddasslem12  40265  paddasslem13  40266  lhpexle3lem  40445  cdlemd4  40635  cdlemefs32sn1aw  40848  cdleme43fsv1snlem  40854  cdleme32d  40878  cdleme32f  40880  cdleme40m  40901  cdleme40n  40902  cdleme50trn2  40985  cdlemftr3  40999  cdlemm10N  41552  dihvalcqpre  41669  dihopelvalcpre  41682  dihmeetlem1N  41724  dihglblem5apreN  41725  dihmeetlem4preN  41740  dihjat1lem  41862  mapd0  42099  mapdh9a  42223  nna4b4nsq  43081  mzpmfp  43167  mzpcompact2lem  43171  diophin  43192  pellexlem3  43247  pellex  43251  pell14qrmulcl  43279  jm2.19lem3  43407  jm2.25  43415  jm2.27b  43422  fnwe2lem2  43467  hbtlem2  43540  hbtlem5  43544  gsumws3  44611  gsumws4  44612  mnuprdlem1  44687  mnuprdlem2  44688  mnuprdlem4  44690  fnchoice  45448  stoweidlem53  46469  stoweidlem61  46477  qndenserrnbllem  46710  bgoldbtbnd  48273  cycldlenngric  48392  grtrimap  48412  isubgr3stgrlem6  48435  prsthinc  49927