Theorem simprrr 779

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  prproe  4838  f1prex  7165  fliftfun  7192  fprresex  8135  wfrlem17OLD  8165  mapdom2  8944  domunfican  9096  fofinf1o  9103  finsschain  9135  wemaplem3  9316  oemapvali  9451  iunfictbso  9879  enfin2i  10086  fin1a2s  10179  distrlem4pr  10791  mulcmpblnr  10836  prsrlem1  10837  addsrmo  10838  mulsrmo  10839  divdivdiv  11685  divsubdiv  11700  lediv12a  11877  xralrple  12948  seqcaopr  13769  leexp2r  13901  hashbclem  14173  wrd2ind  14445  cshwidxmod  14525  rtrclreclem4  14781  relexpindlem  14783  rtrclind  14785  rlimresb  15283  summo  15438  fsum2dlem  15491  prodmo  15655  fprod2dlem  15699  bezoutlem3  16258  bezoutlem4  16259  qredeu  16372  coprmproddvdslem  16376  prmdvdsncoprmbd  16440  pcqmul  16563  pcadd  16599  pockthg  16616  ramub1lem2  16737  cshwsdisj  16809  mreexexlem4d  17365  issubc3  17573  cofucl  17612  setcmon  17811  setcepi  17812  drsdirfi  18032  poslubmo  18138  posglbmo  18139  grpridd  18368  ghmpreima  18865  gaorber  18923  psgnunilem4  19114  psgneu  19123  odcau  19218  pgpssslw  19228  fislw  19239  lsmsubm  19267  efgsfo  19354  pgpfac1  19692  pgpfaclem2  19694  pgpfaclem3  19695  unitgrp  19918  islmodd  20138  lmodprop2d  20194  lsspropd  20288  lbsextlem4  20432  assapropd  21085  evlslem1  21301  mdetunilem8  21777  mdetmul  21781  ppttop  22166  epttop  22168  restbas  22318  iscnp4  22423  cnpco  22427  nrmsep  22517  regsep2  22536  ordthauslem  22543  1stcfb  22605  2ndcctbss  22615  2ndcdisj  22616  2ndcomap  22618  dis2ndc  22620  1stcelcls  22621  nlly2i  22636  islly2  22644  hausllycmp  22654  lly1stc  22656  comppfsc  22692  1stckgenlem  22713  ptbasin  22737  txcls  22764  ptcnp  22782  txlly  22796  txnlly  22797  txtube  22800  txcmplem1  22801  txcmplem2  22802  xkococnlem  22819  basqtop  22871  regr1lem  22899  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  reghmph  22953  nrmhmph  22954  filuni  23045  rnelfmlem  23112  fmufil  23119  fclscf  23185  fclsfnflim  23187  flimfnfcls  23188  uffclsflim  23191  cnpfcfi  23200  cnpfcf  23201  alexsublem  23204  alexsubALTlem3  23209  tgpconncompeqg  23272  ghmcnp  23275  qustgplem  23281  blssps  23586  blss  23587  blcld  23670  metequiv2  23675  met2ndci  23687  prdsxmslem2  23694  txmetcnp  23712  nlmvscnlem1  23859  xrge0tsms  24006  ipcnlem1  24418  iscmet3  24466  metsscmetcld  24488  minveclem3  24602  pmltpc  24623  ovolscalem2  24687  ovolicc2lem5  24694  ovolicc2  24695  nulmbl2  24709  ioombl1  24735  uniioombllem6  24761  uniioombl  24762  vitalilem3  24783  i1faddlem  24866  mbfmullem  24899  itg2const2  24915  itg2split  24923  lhop2  25188  dvfsumrlim  25204  itgsubst  25222  plydivex  25466  plyexmo  25482  ulmbdd  25566  cxploglim  26136  dchrptlem2  26422  lgsquad2lem2  26542  2sqlem5  26579  dchrvmasumif  26660  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem3  26676  dchrisum0  26677  dchrmusum  26681  dchrvmasum  26682  pntibndlem3  26749  pntlemp  26767  ostth3  26795  legtrid  26961  hlcgreu  26988  mirreu3  27024  opphllem  27105  oppperpex  27123  lnperpex  27173  trgcopy  27174  iscgra1  27180  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  acopyeu  27204  ax5seglem9  27314  ax5seg  27315  axcontlem8  27348  axcontlem12  27352  upgrclwlkcompim  28158  wwlksnextwrd  28271  2pthfrgr  28657  frgrnbnb  28666  ablo4  28921  smcnlem  29068  pjhthmo  29673  1stpreimas  31047  xrge0tsmsd  31326  locfinref  31800  xpinpreima2  31866  qqhval2  31941  dya2iocnrect  32257  orvcgteel  32443  orvclteel  32448  cnpconn  33201  txpconn  33203  connpconn  33206  pconnpi1  33208  iccllysconn  33221  rellysconn  33222  cvmcov2  33246  cvmliftmolem2  33253  cvmliftmo  33255  cvmliftlem15  33269  cvmliftpht  33289  cvmlift3lem2  33291  naddssim  33846  nosupbday  33917  nosupbnd1lem1  33920  nosupbnd2  33928  noinfbday  33932  noinfbnd1lem1  33935  noinfbnd2  33943  conway  34002  madebdaylemlrcut  34088  cgrextend  34319  btwnouttr2  34333  btwnexch2  34334  cgrxfr  34366  lineext  34387  btwnconn1lem5  34402  btwnconn1lem13  34410  btwnconn3  34414  segletr  34425  segleantisym  34426  outsideofeq  34441  outsidele  34443  lineunray  34458  refssfne  34556  neibastop2lem  34558  neibastop2  34559  unblimceq0lem  34695  knoppndvlem22  34722  mblfinlem3  35825  mblfinlem4  35826  cnambfre  35834  itg2addnclem  35837  areacirclem5  35878  istotbnd3  35938  crngm4  36170  cvlcvr1  37360  4atlem12  37633  cdlemb  37815  paddasslem10  37850  paddasslem12  37852  paddasslem13  37853  lhpexle3lem  38032  cdlemd4  38222  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme32d  38465  cdleme32f  38467  cdleme40m  38488  cdleme40n  38489  cdleme50trn2  38572  cdlemftr3  38586  cdlemm10N  39139  dihvalcqpre  39256  dihopelvalcpre  39269  dihmeetlem1N  39311  dihglblem5apreN  39312  dihmeetlem4preN  39327  dihjat1lem  39449  mapd0  39686  mapdh9a  39810  nna4b4nsq  40504  mzpmfp  40576  mzpcompact2lem  40580  diophin  40601  pellexlem3  40660  pellex  40664  pell14qrmulcl  40692  jm2.19lem3  40820  jm2.25  40828  jm2.27b  40835  fnwe2lem2  40883  hbtlem2  40956  hbtlem5  40960  gsumws3  41814  gsumws4  41815  mnuprdlem1  41897  mnuprdlem2  41898  mnuprdlem4  41900  fnchoice  42579  stoweidlem53  43601  stoweidlem61  43609  qndenserrnbllem  43842  bgoldbtbnd  45272  prsthinc  46346